Step | Hyp | Ref
| Expression |
1 | | df-tcfn 6108 |
. . 3
⊢ TcFn = (x ∈
1c ↦ Tc ∪x) |
2 | | oteltxp 5783 |
. . . . . . 7
⊢ (⟨z, ⟨{y}, x⟩⟩ ∈ (◡ S ⊗
∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) ↔ (⟨z, {y}⟩ ∈ ◡ S ∧ ⟨z, x⟩ ∈ ∼ ran ( Ins2 ((
NC × V) ∩ ((( S
∘ SI
Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ))) |
3 | | df-br 4641 |
. . . . . . . . 9
⊢ (z◡ S {y} ↔ ⟨z, {y}⟩ ∈ ◡ S ) |
4 | | brcnv 4893 |
. . . . . . . . . 10
⊢ (z◡ S {y} ↔
{y} S z) |
5 | | vex 2863 |
. . . . . . . . . . 11
⊢ y ∈
V |
6 | | vex 2863 |
. . . . . . . . . . 11
⊢ z ∈
V |
7 | 5, 6 | brssetsn 4760 |
. . . . . . . . . 10
⊢ ({y} S z ↔ y ∈ z) |
8 | 4, 7 | bitri 240 |
. . . . . . . . 9
⊢ (z◡ S {y} ↔
y ∈
z) |
9 | 3, 8 | bitr3i 242 |
. . . . . . . 8
⊢ (⟨z, {y}⟩ ∈ ◡ S ↔ y ∈ z) |
10 | | vex 2863 |
. . . . . . . . . . 11
⊢ x ∈
V |
11 | 6, 10 | opex 4589 |
. . . . . . . . . 10
⊢ ⟨z, x⟩ ∈ V |
12 | 11 | elcompl 3226 |
. . . . . . . . 9
⊢ (⟨z, x⟩ ∈ ∼ ran ( Ins2 ((
NC × V) ∩ ((( S
∘ SI
Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ) ↔ ¬ ⟨z, x⟩ ∈ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) |
13 | | elrn2 4898 |
. . . . . . . . . . 11
⊢ (⟨z, x⟩ ∈ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ) ↔ ∃p⟨p, ⟨z, x⟩⟩ ∈ ( Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ⊕
Ins3 I )) |
14 | | elsymdif 3224 |
. . . . . . . . . . . . 13
⊢ (⟨p, ⟨z, x⟩⟩ ∈ ( Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ⊕
Ins3 I ) ↔ ¬ (⟨p, ⟨z, x⟩⟩ ∈ Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ↔ ⟨p, ⟨z, x⟩⟩ ∈ Ins3 I )) |
15 | 6 | otelins2 5792 |
. . . . . . . . . . . . . . 15
⊢ (⟨p, ⟨z, x⟩⟩ ∈ Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ↔ ⟨p, x⟩ ∈ (( NC × V)
∩ ((( S ∘
SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c))) |
16 | | elin 3220 |
. . . . . . . . . . . . . . 15
⊢ (⟨p, x⟩ ∈ (( NC × V)
∩ ((( S ∘
SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ↔ (⟨p, x⟩ ∈ ( NC × V)
∧ ⟨p, x⟩ ∈ ((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c))) |
17 | | opelxp 4812 |
. . . . . . . . . . . . . . . . . 18
⊢ (⟨p, x⟩ ∈ ( NC × V)
↔ (p ∈ NC ∧ x ∈ V)) |
18 | 10, 17 | mpbiran2 885 |
. . . . . . . . . . . . . . . . 17
⊢ (⟨p, x⟩ ∈ ( NC × V)
↔ p ∈ NC
) |
19 | 18 | anbi1i 676 |
. . . . . . . . . . . . . . . 16
⊢ ((⟨p, x⟩ ∈ ( NC × V)
∧ ⟨p, x⟩ ∈ ((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ↔
(p ∈
NC ∧ ⟨p, x⟩ ∈ ((( S ∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c))) |
20 | | ncseqnc 6129 |
. . . . . . . . . . . . . . . . . . 19
⊢ (p ∈ NC → (p = Nc ℘1q ↔ ℘1q ∈ p)) |
21 | 20 | rexbidv 2636 |
. . . . . . . . . . . . . . . . . 18
⊢ (p ∈ NC → (∃q ∈ ∪xp = Nc ℘1q ↔ ∃q ∈ ∪x℘1q ∈ p)) |
22 | | oteltxp 5783 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⟨{{q}}, ⟨p, x⟩⟩ ∈ (( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) ↔ (⟨{{q}},
p⟩ ∈ ( S ∘ SI Pw1Fn ) ∧ ⟨{{q}},
x⟩ ∈ (( SI ◡ S ⊗
S ) “
1c))) |
23 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {q} ∈
V |
24 | 23 | brsnsi1 5776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({{q}} SI Pw1Fn u ↔ ∃t(u = {t} ∧ {q} Pw1Fn t)) |
25 | 24 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (({{q}} SI Pw1Fn u ∧ u S p) ↔ (∃t(u = {t} ∧ {q} Pw1Fn t) ∧ u S p)) |
26 | | 19.41v 1901 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (∃t((u = {t} ∧ {q} Pw1Fn t) ∧ u S p) ↔ (∃t(u = {t} ∧ {q} Pw1Fn t) ∧ u S p)) |
27 | 25, 26 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (({{q}} SI Pw1Fn u ∧ u S p) ↔ ∃t((u = {t} ∧ {q} Pw1Fn t) ∧ u S p)) |
28 | 27 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∃u({{q}} SI Pw1Fn u ∧ u S p) ↔ ∃u∃t((u = {t} ∧ {q} Pw1Fn t) ∧ u S p)) |
29 | | excom 1741 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∃u∃t((u = {t} ∧ {q} Pw1Fn t) ∧ u S p) ↔ ∃t∃u((u = {t} ∧ {q} Pw1Fn t) ∧ u S p)) |
30 | | anass 630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((u = {t} ∧ {q} Pw1Fn t) ∧ u S p) ↔
(u = {t} ∧ ({q} Pw1Fn t ∧ u S p))) |
31 | 30 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (∃u((u = {t} ∧ {q} Pw1Fn t) ∧ u S p) ↔ ∃u(u = {t} ∧ ({q} Pw1Fn t ∧ u S p))) |
32 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ {t} ∈
V |
33 | | breq1 4643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (u = {t} →
(u S p ↔ {t} S p)) |
34 | 33 | anbi2d 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (u = {t} →
(({q} Pw1Fn
t ∧
u S p) ↔ ({q}
Pw1Fn t ∧ {t} S p))) |
35 | 32, 34 | ceqsexv 2895 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (∃u(u = {t} ∧ ({q} Pw1Fn t ∧ u S p)) ↔
({q} Pw1Fn
t ∧
{t} S p)) |
36 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ q ∈
V |
37 | 36 | brpw1fn 5855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({q} Pw1Fn t ↔ t =
℘1q) |
38 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ t ∈
V |
39 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ p ∈
V |
40 | 38, 39 | brssetsn 4760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({t} S p ↔ t ∈ p) |
41 | 37, 40 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (({q} Pw1Fn t ∧ {t} S p) ↔ (t =
℘1q ∧ t ∈ p)) |
42 | 31, 35, 41 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∃u((u = {t} ∧ {q} Pw1Fn t) ∧ u S p) ↔
(t = ℘1q ∧ t ∈ p)) |
43 | 42 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∃t∃u((u = {t} ∧ {q} Pw1Fn t) ∧ u S p) ↔ ∃t(t = ℘1q ∧ t ∈ p)) |
44 | 28, 29, 43 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∃u({{q}} SI Pw1Fn u ∧ u S p) ↔ ∃t(t = ℘1q ∧ t ∈ p)) |
45 | | opelco 4885 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (⟨{{q}},
p⟩ ∈ ( S ∘ SI Pw1Fn ) ↔ ∃u({{q}} SI Pw1Fn u ∧ u S p)) |
46 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (℘1q ∈ p ↔ ∃t(t = ℘1q ∧ t ∈ p)) |
47 | 44, 45, 46 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (⟨{{q}},
p⟩ ∈ ( S ∘ SI Pw1Fn ) ↔ ℘1q ∈ p) |
48 | | oteltxp 5783 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (⟨{t}, ⟨{{q}},
x⟩⟩ ∈ ( SI ◡ S ⊗ S ) ↔
(⟨{t},
{{q}}⟩
∈ SI ◡ S ∧ ⟨{t}, x⟩ ∈ S )) |
49 | | df-br 4641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({t} SI ◡ S {{q}} ↔ ⟨{t},
{{q}}⟩
∈ SI ◡ S
) |
50 | 38, 23 | brsnsi 5774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ({t} SI ◡ S {{q}} ↔ t◡ S {q}) |
51 | | brcnv 4893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (t◡ S {q} ↔
{q} S t) |
52 | 36, 38 | brssetsn 4760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ({q} S t ↔ q ∈ t) |
53 | 50, 51, 52 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({t} SI ◡ S {{q}} ↔ q
∈ t) |
54 | 49, 53 | bitr3i 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (⟨{t},
{{q}}⟩
∈ SI ◡ S ↔
q ∈
t) |
55 | 38, 10 | opelssetsn 4761 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (⟨{t}, x⟩ ∈ S ↔ t ∈ x) |
56 | 54, 55 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((⟨{t},
{{q}}⟩
∈ SI ◡ S ∧ ⟨{t}, x⟩ ∈ S ) ↔ (q ∈ t ∧ t ∈ x)) |
57 | 48, 56 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨{t}, ⟨{{q}},
x⟩⟩ ∈ ( SI ◡ S ⊗ S ) ↔
(q ∈
t ∧
t ∈
x)) |
58 | 57 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∃t⟨{t}, ⟨{{q}},
x⟩⟩ ∈ ( SI ◡ S ⊗ S ) ↔
∃t(q ∈ t ∧ t ∈ x)) |
59 | | elima1c 4948 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (⟨{{q}},
x⟩ ∈ (( SI ◡ S ⊗
S ) “ 1c) ↔ ∃t⟨{t}, ⟨{{q}},
x⟩⟩ ∈ ( SI ◡ S ⊗ S
)) |
60 | | eluni 3895 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (q ∈ ∪x ↔ ∃t(q ∈ t ∧ t ∈ x)) |
61 | 58, 59, 60 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (⟨{{q}},
x⟩ ∈ (( SI ◡ S ⊗
S ) “ 1c) ↔ q ∈ ∪x) |
62 | 47, 61 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((⟨{{q}},
p⟩ ∈ ( S ∘ SI Pw1Fn ) ∧ ⟨{{q}},
x⟩ ∈ (( SI ◡ S ⊗
S ) “ 1c)) ↔ (℘1q ∈ p ∧ q ∈ ∪x)) |
63 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((℘1q ∈ p ∧ q ∈ ∪x) ↔ (q ∈ ∪x ∧ ℘1q ∈ p)) |
64 | 22, 62, 63 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⟨{{q}}, ⟨p, x⟩⟩ ∈ (( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) ↔
(q ∈
∪x ∧ ℘1q ∈ p)) |
65 | 64 | exbii 1582 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃q⟨{{q}}, ⟨p, x⟩⟩ ∈ (( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) ↔ ∃q(q ∈ ∪x ∧ ℘1q ∈ p)) |
66 | | elimapw11c 4949 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⟨p, x⟩ ∈ ((( S ∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c) ↔ ∃q⟨{{q}}, ⟨p, x⟩⟩ ∈ (( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “
1c))) |
67 | | df-rex 2621 |
. . . . . . . . . . . . . . . . . . 19
⊢ (∃q ∈ ∪x℘1q ∈ p ↔ ∃q(q ∈ ∪x ∧ ℘1q ∈ p)) |
68 | 65, 66, 67 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . 18
⊢ (⟨p, x⟩ ∈ ((( S ∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c) ↔ ∃q ∈ ∪x℘1q ∈ p) |
69 | 21, 68 | syl6rbbr 255 |
. . . . . . . . . . . . . . . . 17
⊢ (p ∈ NC → (⟨p, x⟩ ∈ ((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c) ↔ ∃q ∈ ∪xp = Nc ℘1q)) |
70 | 69 | pm5.32i 618 |
. . . . . . . . . . . . . . . 16
⊢ ((p ∈ NC ∧ ⟨p, x⟩ ∈ ((( S ∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ↔
(p ∈
NC ∧ ∃q ∈ ∪xp = Nc ℘1q)) |
71 | 19, 70 | bitri 240 |
. . . . . . . . . . . . . . 15
⊢ ((⟨p, x⟩ ∈ ( NC × V)
∧ ⟨p, x⟩ ∈ ((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ↔
(p ∈
NC ∧ ∃q ∈ ∪xp = Nc ℘1q)) |
72 | 15, 16, 71 | 3bitri 262 |
. . . . . . . . . . . . . 14
⊢ (⟨p, ⟨z, x⟩⟩ ∈ Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ↔
(p ∈
NC ∧ ∃q ∈ ∪xp = Nc ℘1q)) |
73 | 10 | otelins3 5793 |
. . . . . . . . . . . . . . 15
⊢ (⟨p, ⟨z, x⟩⟩ ∈ Ins3 I ↔ ⟨p, z⟩ ∈ I ) |
74 | | df-br 4641 |
. . . . . . . . . . . . . . . 16
⊢ (p I z ↔
⟨p,
z⟩ ∈ I ) |
75 | 6 | ideq 4871 |
. . . . . . . . . . . . . . . 16
⊢ (p I z ↔
p = z) |
76 | 74, 75 | bitr3i 242 |
. . . . . . . . . . . . . . 15
⊢ (⟨p, z⟩ ∈ I ↔ p =
z) |
77 | 73, 76 | bitri 240 |
. . . . . . . . . . . . . 14
⊢ (⟨p, ⟨z, x⟩⟩ ∈ Ins3 I ↔ p =
z) |
78 | 72, 77 | bibi12i 306 |
. . . . . . . . . . . . 13
⊢ ((⟨p, ⟨z, x⟩⟩ ∈ Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ↔ ⟨p, ⟨z, x⟩⟩ ∈ Ins3 I ) ↔ ((p
∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)) |
79 | 14, 78 | xchbinx 301 |
. . . . . . . . . . . 12
⊢ (⟨p, ⟨z, x⟩⟩ ∈ ( Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ⊕
Ins3 I ) ↔ ¬ ((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)) |
80 | 79 | exbii 1582 |
. . . . . . . . . . 11
⊢ (∃p⟨p, ⟨z, x⟩⟩ ∈ ( Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ⊕
Ins3 I ) ↔ ∃p ¬
((p ∈
NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)) |
81 | | exnal 1574 |
. . . . . . . . . . 11
⊢ (∃p ¬
((p ∈
NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z) ↔ ¬ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)) |
82 | 13, 80, 81 | 3bitrri 263 |
. . . . . . . . . 10
⊢ (¬ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z) ↔ ⟨z, x⟩ ∈ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) |
83 | 82 | con1bii 321 |
. . . . . . . . 9
⊢ (¬ ⟨z, x⟩ ∈ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ) ↔ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)) |
84 | 12, 83 | bitri 240 |
. . . . . . . 8
⊢ (⟨z, x⟩ ∈ ∼ ran ( Ins2 ((
NC × V) ∩ ((( S
∘ SI
Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ) ↔ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)) |
85 | 9, 84 | anbi12i 678 |
. . . . . . 7
⊢ ((⟨z, {y}⟩ ∈ ◡ S ∧ ⟨z, x⟩ ∈ ∼ ran ( Ins2 ((
NC × V) ∩ ((( S
∘ SI
Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) ↔ (y ∈ z ∧ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z))) |
86 | 2, 85 | bitri 240 |
. . . . . 6
⊢ (⟨z, ⟨{y}, x⟩⟩ ∈ (◡ S ⊗
∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) ↔ (y ∈ z ∧ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z))) |
87 | 86 | exbii 1582 |
. . . . 5
⊢ (∃z⟨z, ⟨{y}, x⟩⟩ ∈ (◡ S ⊗
∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) ↔ ∃z(y ∈ z ∧ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z))) |
88 | | elrn2 4898 |
. . . . 5
⊢ (⟨{y}, x⟩ ∈ ran (◡ S ⊗
∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) ↔ ∃z⟨z, ⟨{y}, x⟩⟩ ∈ (◡ S ⊗
∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ))) |
89 | | df-tc 6104 |
. . . . . . . 8
⊢ Tc ∪x = (℩p(p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q)) |
90 | | dfiota2 4341 |
. . . . . . . 8
⊢ (℩p(p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q)) = ∪{z ∣ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)} |
91 | 89, 90 | eqtri 2373 |
. . . . . . 7
⊢ Tc ∪x = ∪{z ∣ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)} |
92 | 91 | eleq2i 2417 |
. . . . . 6
⊢ (y ∈ Tc ∪x ↔ y ∈ ∪{z ∣ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)}) |
93 | | eluniab 3904 |
. . . . . 6
⊢ (y ∈ ∪{z ∣ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z)} ↔ ∃z(y ∈ z ∧ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z))) |
94 | 92, 93 | bitri 240 |
. . . . 5
⊢ (y ∈ Tc ∪x ↔ ∃z(y ∈ z ∧ ∀p((p ∈ NC ∧ ∃q ∈ ∪xp = Nc ℘1q) ↔ p =
z))) |
95 | 87, 88, 94 | 3bitr4i 268 |
. . . 4
⊢ (⟨{y}, x⟩ ∈ ran (◡ S ⊗
∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) ↔ y ∈ Tc ∪x) |
96 | 95 | releqmpt 5809 |
. . 3
⊢
((1c × V) ∩ ◡ ∼ (( Ins3
S ⊕ Ins2 ran
(◡ S
⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ))) “ 1c)) =
(x ∈
1c ↦ Tc ∪x) |
97 | 1, 96 | eqtr4i 2376 |
. 2
⊢ TcFn =
((1c × V) ∩ ◡ ∼ (( Ins3
S ⊕ Ins2 ran
(◡ S
⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ))) “
1c)) |
98 | | 1cex 4143 |
. . 3
⊢
1c ∈
V |
99 | | ssetex 4745 |
. . . . . 6
⊢ S ∈
V |
100 | 99 | cnvex 5103 |
. . . . 5
⊢ ◡ S ∈ V |
101 | | ncsex 6112 |
. . . . . . . . . . 11
⊢ NC ∈
V |
102 | | vvex 4110 |
. . . . . . . . . . 11
⊢ V ∈ V |
103 | 101, 102 | xpex 5116 |
. . . . . . . . . 10
⊢ ( NC × V) ∈
V |
104 | | pw1fnex 5853 |
. . . . . . . . . . . . . 14
⊢ Pw1Fn ∈
V |
105 | 104 | siex 4754 |
. . . . . . . . . . . . 13
⊢ SI Pw1Fn ∈ V |
106 | 99, 105 | coex 4751 |
. . . . . . . . . . . 12
⊢ ( S ∘ SI Pw1Fn ) ∈ V |
107 | 100 | siex 4754 |
. . . . . . . . . . . . . 14
⊢ SI ◡ S ∈
V |
108 | 107, 99 | txpex 5786 |
. . . . . . . . . . . . 13
⊢ ( SI ◡ S ⊗ S ) ∈ V |
109 | 108, 98 | imaex 4748 |
. . . . . . . . . . . 12
⊢ (( SI ◡ S ⊗ S ) “
1c) ∈ V |
110 | 106, 109 | txpex 5786 |
. . . . . . . . . . 11
⊢ (( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) ∈ V |
111 | 98 | pw1ex 4304 |
. . . . . . . . . . 11
⊢ ℘11c ∈ V |
112 | 110, 111 | imaex 4748 |
. . . . . . . . . 10
⊢ ((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c) ∈ V |
113 | 103, 112 | inex 4106 |
. . . . . . . . 9
⊢ (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ∈ V |
114 | 113 | ins2ex 5798 |
. . . . . . . 8
⊢ Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ∈ V |
115 | | idex 5505 |
. . . . . . . . 9
⊢ I ∈ V |
116 | 115 | ins3ex 5799 |
. . . . . . . 8
⊢ Ins3 I ∈
V |
117 | 114, 116 | symdifex 4109 |
. . . . . . 7
⊢ ( Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ⊕
Ins3 I ) ∈
V |
118 | 117 | rnex 5108 |
. . . . . 6
⊢ ran ( Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ⊕
Ins3 I ) ∈
V |
119 | 118 | complex 4105 |
. . . . 5
⊢ ∼ ran ( Ins2 (( NC × V) ∩
((( S ∘ SI Pw1Fn ) ⊗
(( SI ◡ S ⊗
S ) “ 1c)) “ ℘11c)) ⊕
Ins3 I ) ∈
V |
120 | 100, 119 | txpex 5786 |
. . . 4
⊢ (◡ S ⊗
∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) ∈
V |
121 | 120 | rnex 5108 |
. . 3
⊢ ran (◡ S ⊗
∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I )) ∈
V |
122 | 98, 121 | mptexlem 5811 |
. 2
⊢
((1c × V) ∩ ◡ ∼ (( Ins3
S ⊕ Ins2 ran
(◡ S
⊗ ∼ ran ( Ins2 (( NC × V) ∩ ((( S
∘ SI Pw1Fn ) ⊗ (( SI
◡ S
⊗ S ) “
1c)) “ ℘11c)) ⊕
Ins3 I ))) “ 1c)) ∈ V |
123 | 97, 122 | eqeltri 2423 |
1
⊢ TcFn ∈ V |