Step | Hyp | Ref
| Expression |
1 | | pm2.1 406 |
. . . 4
⊢ (¬ x ∈ NC ∨ x ∈ NC ) |
2 | | fnspac 6283 |
. . . . . . . . . . 11
⊢ Spac Fn NC |
3 | | fndm 5182 |
. . . . . . . . . . 11
⊢ ( Spac Fn NC
→ dom Spac = NC ) |
4 | 2, 3 | ax-mp 8 |
. . . . . . . . . 10
⊢ dom Spac = NC |
5 | 4 | eleq2i 2417 |
. . . . . . . . 9
⊢ (x ∈ dom Spac ↔ x ∈ NC ) |
6 | | ndmfv 5349 |
. . . . . . . . 9
⊢ (¬ x ∈ dom Spac → ( Spac ‘x) = ∅) |
7 | 5, 6 | sylnbir 298 |
. . . . . . . 8
⊢ (¬ x ∈ NC → ( Spac
‘x) = ∅) |
8 | | 0fin 4423 |
. . . . . . . 8
⊢ ∅ ∈ Fin |
9 | 7, 8 | syl6eqel 2441 |
. . . . . . 7
⊢ (¬ x ∈ NC → ( Spac
‘x) ∈ Fin
) |
10 | 9 | pm4.71i 613 |
. . . . . 6
⊢ (¬ x ∈ NC ↔ (¬ x
∈ NC ∧ ( Spac
‘x) ∈ Fin
)) |
11 | 10 | orbi1i 506 |
. . . . 5
⊢ ((¬ x ∈ NC ∨ (x ∈ NC ∧ ( Spac ‘x) ∈ Fin )) ↔ ((¬ x ∈ NC ∧ ( Spac ‘x) ∈ Fin ) ∨ (x ∈ NC ∧ ( Spac ‘x) ∈ Fin ))) |
12 | | elun 3220 |
. . . . . 6
⊢ (x ∈ ( ∼ NC ∪ ( NC ∩
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ))) ↔ (x
∈ ∼ NC ∨ x ∈ ( NC ∩
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin )))) |
13 | | vex 2862 |
. . . . . . . 8
⊢ x ∈
V |
14 | 13 | elcompl 3225 |
. . . . . . 7
⊢ (x ∈ ∼ NC ↔ ¬ x
∈ NC
) |
15 | | elin 3219 |
. . . . . . . 8
⊢ (x ∈ ( NC ∩ ⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin )) ↔ (x
∈ NC ∧ x ∈ ⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ))) |
16 | | spacval 6282 |
. . . . . . . . . . 11
⊢ (x ∈ NC → ( Spac
‘x) = Clos1
({x}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})) |
17 | 16 | eleq1d 2419 |
. . . . . . . . . 10
⊢ (x ∈ NC → (( Spac ‘x) ∈ Fin ↔ Clos1
({x}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) ∈ Fin )) |
18 | 13 | eluni1 4173 |
. . . . . . . . . . 11
⊢ (x ∈
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ) ↔ {x}
∈ ( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin )) |
19 | | df-br 4640 |
. . . . . . . . . . . . . 14
⊢ (c ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c){x} ↔ 〈c, {x}〉 ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “
1c)) |
20 | | spacvallem1 6281 |
. . . . . . . . . . . . . . 15
⊢ {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))} ∈
V |
21 | | snex 4111 |
. . . . . . . . . . . . . . 15
⊢ {x} ∈
V |
22 | 20, 21 | nchoicelem10 6298 |
. . . . . . . . . . . . . 14
⊢ (〈c, {x}〉 ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) ↔
c = Clos1
({x}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})) |
23 | 19, 22 | bitri 240 |
. . . . . . . . . . . . 13
⊢ (c ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c){x} ↔ c =
Clos1 ({x},
{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})) |
24 | 23 | rexbii 2639 |
. . . . . . . . . . . 12
⊢ (∃c ∈ Fin c ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c){x} ↔ ∃c ∈ Fin c = Clos1 ({x}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q = (2c ↑c
p))})) |
25 | | elima 4754 |
. . . . . . . . . . . 12
⊢ ({x} ∈ ( ∼ ((
Ins3 S ⊕
Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ) ↔ ∃c ∈ Fin c ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c){x}) |
26 | | risset 2661 |
. . . . . . . . . . . 12
⊢ ( Clos1 ({x}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) ∈ Fin ↔ ∃c ∈ Fin c = Clos1 ({x}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})) |
27 | 24, 25, 26 | 3bitr4i 268 |
. . . . . . . . . . 11
⊢ ({x} ∈ ( ∼ ((
Ins3 S ⊕
Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ) ↔ Clos1
({x}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) ∈ Fin ) |
28 | 18, 27 | bitri 240 |
. . . . . . . . . 10
⊢ (x ∈
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ) ↔ Clos1
({x}, {〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) ∈ Fin ) |
29 | 17, 28 | syl6rbbr 255 |
. . . . . . . . 9
⊢ (x ∈ NC → (x ∈ ⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ) ↔ ( Spac ‘x) ∈ Fin )) |
30 | 29 | pm5.32i 618 |
. . . . . . . 8
⊢ ((x ∈ NC ∧ x ∈
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin )) ↔ (x
∈ NC ∧ ( Spac
‘x) ∈ Fin
)) |
31 | 15, 30 | bitri 240 |
. . . . . . 7
⊢ (x ∈ ( NC ∩ ⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin )) ↔ (x
∈ NC ∧ ( Spac
‘x) ∈ Fin
)) |
32 | 14, 31 | orbi12i 507 |
. . . . . 6
⊢ ((x ∈ ∼ NC ∨ x ∈ ( NC ∩ ⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ))) ↔ (¬ x ∈ NC ∨ (x ∈ NC ∧ ( Spac ‘x) ∈ Fin ))) |
33 | 12, 32 | bitri 240 |
. . . . 5
⊢ (x ∈ ( ∼ NC ∪ ( NC ∩
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ))) ↔ (¬ x ∈ NC ∨ (x ∈ NC ∧ ( Spac ‘x) ∈ Fin ))) |
34 | | andir 838 |
. . . . 5
⊢ (((¬ x ∈ NC ∨ x ∈ NC ) ∧ ( Spac ‘x) ∈ Fin ) ↔ ((¬ x ∈ NC ∧ ( Spac ‘x) ∈ Fin ) ∨ (x ∈ NC ∧ ( Spac ‘x) ∈ Fin ))) |
35 | 11, 33, 34 | 3bitr4i 268 |
. . . 4
⊢ (x ∈ ( ∼ NC ∪ ( NC ∩
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ))) ↔ ((¬ x ∈ NC ∨ x ∈ NC ) ∧ ( Spac ‘x) ∈ Fin )) |
36 | 1, 35 | mpbiran 884 |
. . 3
⊢ (x ∈ ( ∼ NC ∪ ( NC ∩
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ))) ↔ ( Spac ‘x) ∈ Fin ) |
37 | 36 | abbi2i 2464 |
. 2
⊢ ( ∼ NC ∪ ( NC ∩
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ))) = {x ∣ ( Spac
‘x) ∈ Fin
} |
38 | | ncsex 6111 |
. . . 4
⊢ NC ∈
V |
39 | 38 | complex 4104 |
. . 3
⊢ ∼ NC ∈
V |
40 | | ssetex 4744 |
. . . . . . . . . 10
⊢ S ∈
V |
41 | 40 | ins3ex 5798 |
. . . . . . . . 9
⊢ Ins3 S ∈ V |
42 | 40 | complex 4104 |
. . . . . . . . . . . . . 14
⊢ ∼ S ∈
V |
43 | 42 | cnvex 5102 |
. . . . . . . . . . . . 13
⊢ ◡ ∼ S
∈ V |
44 | 40 | cnvex 5102 |
. . . . . . . . . . . . . 14
⊢ ◡ S ∈ V |
45 | 20 | imageex 5801 |
. . . . . . . . . . . . . . . 16
⊢ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))} ∈
V |
46 | 40, 45 | coex 4750 |
. . . . . . . . . . . . . . 15
⊢ ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) ∈
V |
47 | 46 | fixex 5789 |
. . . . . . . . . . . . . 14
⊢ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}) ∈
V |
48 | 44, 47 | resex 5117 |
. . . . . . . . . . . . 13
⊢ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})) ∈
V |
49 | 43, 48 | txpex 5785 |
. . . . . . . . . . . 12
⊢ (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}))) ∈
V |
50 | 49 | rnex 5107 |
. . . . . . . . . . 11
⊢ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}))) ∈
V |
51 | 50 | complex 4104 |
. . . . . . . . . 10
⊢ ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}))) ∈
V |
52 | 51 | ins2ex 5797 |
. . . . . . . . 9
⊢ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))}))) ∈
V |
53 | 41, 52 | symdifex 4108 |
. . . . . . . 8
⊢ ( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) ∈
V |
54 | | 1cex 4142 |
. . . . . . . 8
⊢
1c ∈
V |
55 | 53, 54 | imaex 4747 |
. . . . . . 7
⊢ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) ∈ V |
56 | 55 | complex 4104 |
. . . . . 6
⊢ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) ∈ V |
57 | | finex 4397 |
. . . . . 6
⊢ Fin ∈
V |
58 | 56, 57 | imaex 4747 |
. . . . 5
⊢ ( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ) ∈
V |
59 | 58 | uni1ex 4293 |
. . . 4
⊢ ⋃1(
∼ (( Ins3 S
⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ) ∈
V |
60 | 38, 59 | inex 4105 |
. . 3
⊢ ( NC ∩ ⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
Image{〈p,
q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin )) ∈
V |
61 | 39, 60 | unex 4106 |
. 2
⊢ ( ∼ NC ∪ ( NC ∩
⋃1( ∼ (( Ins3 S ⊕ Ins2 ∼ ran
(◡ ∼ S
⊗ (◡ S ↾ Fix ( S ∘ Image{〈p, q〉 ∣ (p ∈ NC ∧ q ∈ NC ∧ q =
(2c ↑c p))})))) “ 1c) “ Fin ))) ∈
V |
62 | 37, 61 | eqeltrri 2424 |
1
⊢ {x ∣ ( Spac ‘x) ∈ Fin } ∈
V |