Step | Hyp | Ref
| Expression |
1 | | snex 4835 |
. . . 4
⊢ {(𝐴 “ {𝐵})} ∈ V |
2 | 1 | inex1 4727 |
. . 3
⊢ ({(𝐴 “ {𝐵})} ∩ Singletons
) ∈ V |
3 | | unieq 4380 |
. . . . 5
⊢ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) → ∪ 𝑥 = ∪ ({(𝐴 “ {𝐵})} ∩ Singletons
)) |
4 | 3 | unieqd 4382 |
. . . 4
⊢ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) → ∪ ∪ 𝑥 = ∪
∪ ({(𝐴 “ {𝐵})} ∩ Singletons
)) |
5 | 4 | eqeq2d 2620 |
. . 3
⊢ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) → (𝐶 = ∪ ∪ 𝑥 ↔ 𝐶 = ∪ ∪ ({(𝐴
“ {𝐵})} ∩ Singletons ))) |
6 | 2, 5 | ceqsexv 3215 |
. 2
⊢
(∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) ∧ 𝐶 = ∪ ∪ 𝑥) ↔ 𝐶 = ∪ ∪ ({(𝐴
“ {𝐵})} ∩ Singletons )) |
7 | | df-apply 31149 |
. . . 4
⊢ Apply =
(( Bigcup ∘ Bigcup
) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E
↾ Singletons ) ⊗ V))) ∘
((Singleton ∘ Img) ∘ pprod( I , Singleton)))) |
8 | 7 | breqi 4589 |
. . 3
⊢
(〈𝐴, 𝐵〉Apply𝐶 ↔ 〈𝐴, 𝐵〉(( Bigcup
∘ Bigcup ) ∘ (((V × V)
∖ ran ((V ⊗ E ) △ (( E ↾
Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘
pprod( I , Singleton))))𝐶) |
9 | | opex 4859 |
. . . 4
⊢
〈𝐴, 𝐵〉 ∈ V |
10 | | brapply.3 |
. . . 4
⊢ 𝐶 ∈ V |
11 | 9, 10 | brco 5214 |
. . 3
⊢
(〈𝐴, 𝐵〉((
Bigcup ∘ Bigcup ) ∘ (((V
× V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘
Img) ∘ pprod( I , Singleton))))𝐶 ↔ ∃𝑥(〈𝐴, 𝐵〉(((V × V) ∖ ran ((V
⊗ E ) △ (( E ↾ Singletons )
⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I ,
Singleton)))𝑥 ∧ 𝑥( Bigcup
∘ Bigcup )𝐶)) |
12 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
13 | 9, 12 | brco 5214 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉(((V × V) ∖
ran ((V ⊗ E ) △ (( E ↾ Singletons
) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I ,
Singleton)))𝑥 ↔
∃𝑦(〈𝐴, 𝐵〉((Singleton ∘ Img) ∘
pprod( I , Singleton))𝑦
∧ 𝑦((V × V)
∖ ran ((V ⊗ E ) △ (( E ↾
Singletons ) ⊗ V)))𝑥)) |
14 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
15 | 9, 14 | brco 5214 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉((Singleton ∘ Img)
∘ pprod( I , Singleton))𝑦 ↔ ∃𝑧(〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ∧ 𝑧(Singleton ∘ Img)𝑦)) |
16 | | brapply.1 |
. . . . . . . . . . . . 13
⊢ 𝐴 ∈ V |
17 | | brapply.2 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ V |
18 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
19 | 16, 17, 18 | brpprod3a 31163 |
. . . . . . . . . . . 12
⊢
(〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ↔ ∃𝑎∃𝑏(𝑧 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐵Singleton𝑏)) |
20 | | 3anrot 1036 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐵Singleton𝑏) ↔ (𝐴 I 𝑎 ∧ 𝐵Singleton𝑏 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
21 | | vex 3176 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑎 ∈ V |
22 | 21 | ideq 5196 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 I 𝑎 ↔ 𝐴 = 𝑎) |
23 | | eqcom 2617 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = 𝑎 ↔ 𝑎 = 𝐴) |
24 | 22, 23 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 I 𝑎 ↔ 𝑎 = 𝐴) |
25 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑏 ∈ V |
26 | 17, 25 | brsingle 31194 |
. . . . . . . . . . . . . . 15
⊢ (𝐵Singleton𝑏 ↔ 𝑏 = {𝐵}) |
27 | | biid 250 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑎, 𝑏〉 ↔ 𝑧 = 〈𝑎, 𝑏〉) |
28 | 24, 26, 27 | 3anbi123i 1244 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 I 𝑎 ∧ 𝐵Singleton𝑏 ∧ 𝑧 = 〈𝑎, 𝑏〉) ↔ (𝑎 = 𝐴 ∧ 𝑏 = {𝐵} ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
29 | 20, 28 | bitri 263 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐵Singleton𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = {𝐵} ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
30 | 29 | 2exbii 1765 |
. . . . . . . . . . . 12
⊢
(∃𝑎∃𝑏(𝑧 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐵Singleton𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = {𝐵} ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
31 | | snex 4835 |
. . . . . . . . . . . . 13
⊢ {𝐵} ∈ V |
32 | | opeq1 4340 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
33 | 32 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → (𝑧 = 〈𝑎, 𝑏〉 ↔ 𝑧 = 〈𝐴, 𝑏〉)) |
34 | | opeq2 4341 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = {𝐵} → 〈𝐴, 𝑏〉 = 〈𝐴, {𝐵}〉) |
35 | 34 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑏 = {𝐵} → (𝑧 = 〈𝐴, 𝑏〉 ↔ 𝑧 = 〈𝐴, {𝐵}〉)) |
36 | 16, 31, 33, 35 | ceqsex2v 3218 |
. . . . . . . . . . . 12
⊢
(∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = {𝐵} ∧ 𝑧 = 〈𝑎, 𝑏〉) ↔ 𝑧 = 〈𝐴, {𝐵}〉) |
37 | 19, 30, 36 | 3bitri 285 |
. . . . . . . . . . 11
⊢
(〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ↔ 𝑧 = 〈𝐴, {𝐵}〉) |
38 | 37 | anbi1i 727 |
. . . . . . . . . 10
⊢
((〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ (𝑧 = 〈𝐴, {𝐵}〉 ∧ 𝑧(Singleton ∘ Img)𝑦)) |
39 | 38 | exbii 1764 |
. . . . . . . . 9
⊢
(∃𝑧(〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ ∃𝑧(𝑧 = 〈𝐴, {𝐵}〉 ∧ 𝑧(Singleton ∘ Img)𝑦)) |
40 | | opex 4859 |
. . . . . . . . . . 11
⊢
〈𝐴, {𝐵}〉 ∈
V |
41 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝐴, {𝐵}〉 → (𝑧(Singleton ∘ Img)𝑦 ↔ 〈𝐴, {𝐵}〉(Singleton ∘ Img)𝑦)) |
42 | 40, 41 | ceqsexv 3215 |
. . . . . . . . . 10
⊢
(∃𝑧(𝑧 = 〈𝐴, {𝐵}〉 ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ 〈𝐴, {𝐵}〉(Singleton ∘ Img)𝑦) |
43 | 40, 14 | brco 5214 |
. . . . . . . . . 10
⊢
(〈𝐴, {𝐵}〉(Singleton ∘
Img)𝑦 ↔ ∃𝑥(〈𝐴, {𝐵}〉Img𝑥 ∧ 𝑥Singleton𝑦)) |
44 | 16, 31, 12 | brimg 31214 |
. . . . . . . . . . . . 13
⊢
(〈𝐴, {𝐵}〉Img𝑥 ↔ 𝑥 = (𝐴 “ {𝐵})) |
45 | 12, 14 | brsingle 31194 |
. . . . . . . . . . . . 13
⊢ (𝑥Singleton𝑦 ↔ 𝑦 = {𝑥}) |
46 | 44, 45 | anbi12i 729 |
. . . . . . . . . . . 12
⊢
((〈𝐴, {𝐵}〉Img𝑥 ∧ 𝑥Singleton𝑦) ↔ (𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥})) |
47 | 46 | exbii 1764 |
. . . . . . . . . . 11
⊢
(∃𝑥(〈𝐴, {𝐵}〉Img𝑥 ∧ 𝑥Singleton𝑦) ↔ ∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥})) |
48 | | imaexg 6995 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ V → (𝐴 “ {𝐵}) ∈ V) |
49 | 16, 48 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐴 “ {𝐵}) ∈ V |
50 | | sneq 4135 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 “ {𝐵}) → {𝑥} = {(𝐴 “ {𝐵})}) |
51 | 50 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐴 “ {𝐵}) → (𝑦 = {𝑥} ↔ 𝑦 = {(𝐴 “ {𝐵})})) |
52 | 49, 51 | ceqsexv 3215 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}) ↔ 𝑦 = {(𝐴 “ {𝐵})}) |
53 | 47, 52 | bitri 263 |
. . . . . . . . . 10
⊢
(∃𝑥(〈𝐴, {𝐵}〉Img𝑥 ∧ 𝑥Singleton𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})}) |
54 | 42, 43, 53 | 3bitri 285 |
. . . . . . . . 9
⊢
(∃𝑧(𝑧 = 〈𝐴, {𝐵}〉 ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})}) |
55 | 15, 39, 54 | 3bitri 285 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉((Singleton ∘ Img)
∘ pprod( I , Singleton))𝑦 ↔ 𝑦 = {(𝐴 “ {𝐵})}) |
56 | | eqid 2610 |
. . . . . . . . 9
⊢ ((V
× V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) = ((V × V) ∖ ran
((V ⊗ E ) △ (( E ↾ Singletons
) ⊗ V))) |
57 | | brxp 5071 |
. . . . . . . . . 10
⊢ (𝑦(V × V)𝑥 ↔ (𝑦 ∈ V ∧ 𝑥 ∈ V)) |
58 | 14, 12, 57 | mpbir2an 957 |
. . . . . . . . 9
⊢ 𝑦(V × V)𝑥 |
59 | | epel 4952 |
. . . . . . . . . . 11
⊢ (𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦) |
60 | 59 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑧 E 𝑦 ∧ 𝑧 ∈ Singletons
) ↔ (𝑧 ∈
𝑦 ∧ 𝑧 ∈ Singletons
)) |
61 | 14 | brres 5323 |
. . . . . . . . . 10
⊢ (𝑧( E ↾ Singletons )𝑦 ↔ (𝑧 E 𝑦 ∧ 𝑧 ∈ Singletons
)) |
62 | | elin 3758 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑦 ∩ Singletons
) ↔ (𝑧 ∈
𝑦 ∧ 𝑧 ∈ Singletons
)) |
63 | 60, 61, 62 | 3bitr4ri 292 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑦 ∩ Singletons
) ↔ 𝑧( E
↾ Singletons )𝑦) |
64 | 14, 12, 56, 58, 63 | brtxpsd3 31173 |
. . . . . . . 8
⊢ (𝑦((V × V) ∖ ran ((V
⊗ E ) △ (( E ↾ Singletons )
⊗ V)))𝑥 ↔ 𝑥 = (𝑦 ∩ Singletons
)) |
65 | 55, 64 | anbi12i 729 |
. . . . . . 7
⊢
((〈𝐴, 𝐵〉((Singleton ∘ Img)
∘ pprod( I , Singleton))𝑦 ∧ 𝑦((V × V) ∖ ran ((V ⊗ E )
△ (( E ↾ Singletons ) ⊗
V)))𝑥) ↔ (𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 ∩ Singletons
))) |
66 | 65 | exbii 1764 |
. . . . . 6
⊢
(∃𝑦(〈𝐴, 𝐵〉((Singleton ∘ Img) ∘
pprod( I , Singleton))𝑦
∧ 𝑦((V × V)
∖ ran ((V ⊗ E ) △ (( E ↾
Singletons ) ⊗ V)))𝑥) ↔ ∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 ∩ Singletons
))) |
67 | | ineq1 3769 |
. . . . . . . 8
⊢ (𝑦 = {(𝐴 “ {𝐵})} → (𝑦 ∩ Singletons
) = ({(𝐴 “
{𝐵})} ∩ Singletons )) |
68 | 67 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑦 = {(𝐴 “ {𝐵})} → (𝑥 = (𝑦 ∩ Singletons
) ↔ 𝑥 =
({(𝐴 “ {𝐵})} ∩
Singletons ))) |
69 | 1, 68 | ceqsexv 3215 |
. . . . . 6
⊢
(∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 ∩ Singletons
)) ↔ 𝑥 =
({(𝐴 “ {𝐵})} ∩
Singletons )) |
70 | 13, 66, 69 | 3bitri 285 |
. . . . 5
⊢
(〈𝐴, 𝐵〉(((V × V) ∖
ran ((V ⊗ E ) △ (( E ↾ Singletons
) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I ,
Singleton)))𝑥 ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
)) |
71 | 12, 10 | brco 5214 |
. . . . . 6
⊢ (𝑥( Bigcup
∘ Bigcup )𝐶 ↔ ∃𝑦(𝑥 Bigcup 𝑦 ∧ 𝑦 Bigcup 𝐶)) |
72 | 14 | brbigcup 31175 |
. . . . . . . . 9
⊢ (𝑥 Bigcup
𝑦 ↔ ∪ 𝑥 =
𝑦) |
73 | | eqcom 2617 |
. . . . . . . . 9
⊢ (∪ 𝑥 =
𝑦 ↔ 𝑦 = ∪ 𝑥) |
74 | 72, 73 | bitri 263 |
. . . . . . . 8
⊢ (𝑥 Bigcup
𝑦 ↔ 𝑦 = ∪
𝑥) |
75 | 10 | brbigcup 31175 |
. . . . . . . . 9
⊢ (𝑦 Bigcup
𝐶 ↔ ∪ 𝑦 =
𝐶) |
76 | | eqcom 2617 |
. . . . . . . . 9
⊢ (∪ 𝑦 =
𝐶 ↔ 𝐶 = ∪ 𝑦) |
77 | 75, 76 | bitri 263 |
. . . . . . . 8
⊢ (𝑦 Bigcup
𝐶 ↔ 𝐶 = ∪
𝑦) |
78 | 74, 77 | anbi12i 729 |
. . . . . . 7
⊢ ((𝑥 Bigcup
𝑦 ∧ 𝑦 Bigcup
𝐶) ↔ (𝑦 = ∪
𝑥 ∧ 𝐶 = ∪ 𝑦)) |
79 | 78 | exbii 1764 |
. . . . . 6
⊢
(∃𝑦(𝑥 Bigcup
𝑦 ∧ 𝑦 Bigcup
𝐶) ↔
∃𝑦(𝑦 = ∪ 𝑥 ∧ 𝐶 = ∪ 𝑦)) |
80 | | vuniex 6852 |
. . . . . . 7
⊢ ∪ 𝑥
∈ V |
81 | | unieq 4380 |
. . . . . . . 8
⊢ (𝑦 = ∪
𝑥 → ∪ 𝑦 =
∪ ∪ 𝑥) |
82 | 81 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑦 = ∪
𝑥 → (𝐶 = ∪ 𝑦 ↔ 𝐶 = ∪ ∪ 𝑥)) |
83 | 80, 82 | ceqsexv 3215 |
. . . . . 6
⊢
(∃𝑦(𝑦 = ∪
𝑥 ∧ 𝐶 = ∪ 𝑦) ↔ 𝐶 = ∪ ∪ 𝑥) |
84 | 71, 79, 83 | 3bitri 285 |
. . . . 5
⊢ (𝑥( Bigcup
∘ Bigcup )𝐶 ↔ 𝐶 = ∪ ∪ 𝑥) |
85 | 70, 84 | anbi12i 729 |
. . . 4
⊢
((〈𝐴, 𝐵〉(((V × V) ∖
ran ((V ⊗ E ) △ (( E ↾ Singletons
) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I ,
Singleton)))𝑥 ∧ 𝑥( Bigcup
∘ Bigcup )𝐶) ↔ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) ∧ 𝐶 = ∪ ∪ 𝑥)) |
86 | 85 | exbii 1764 |
. . 3
⊢
(∃𝑥(〈𝐴, 𝐵〉(((V × V) ∖ ran ((V
⊗ E ) △ (( E ↾ Singletons )
⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I ,
Singleton)))𝑥 ∧ 𝑥( Bigcup
∘ Bigcup )𝐶) ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) ∧ 𝐶 = ∪ ∪ 𝑥)) |
87 | 8, 11, 86 | 3bitri 285 |
. 2
⊢
(〈𝐴, 𝐵〉Apply𝐶 ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) ∧ 𝐶 = ∪ ∪ 𝑥)) |
88 | | dffv5 31201 |
. . 3
⊢ (𝐴‘𝐵) = ∪ ∪ ({(𝐴
“ {𝐵})} ∩ Singletons ) |
89 | 88 | eqeq2i 2622 |
. 2
⊢ (𝐶 = (𝐴‘𝐵) ↔ 𝐶 = ∪ ∪ ({(𝐴
“ {𝐵})} ∩ Singletons )) |
90 | 6, 87, 89 | 3bitr4i 291 |
1
⊢
(〈𝐴, 𝐵〉Apply𝐶 ↔ 𝐶 = (𝐴‘𝐵)) |