| Step | Hyp | Ref
| Expression |
| 1 | | snex 5436 |
. . . 4
⊢ {(𝐴 “ {𝐵})} ∈ V |
| 2 | 1 | inex1 5317 |
. . 3
⊢ ({(𝐴 “ {𝐵})} ∩ Singletons
) ∈ V |
| 3 | | unieq 4918 |
. . . . 5
⊢ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) → ∪ 𝑥 = ∪ ({(𝐴 “ {𝐵})} ∩ Singletons
)) |
| 4 | 3 | unieqd 4920 |
. . . 4
⊢ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) → ∪ ∪ 𝑥 = ∪
∪ ({(𝐴 “ {𝐵})} ∩ Singletons
)) |
| 5 | 4 | eqeq2d 2748 |
. . 3
⊢ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) → (𝐶 = ∪ ∪ 𝑥 ↔ 𝐶 = ∪ ∪ ({(𝐴
“ {𝐵})} ∩ Singletons ))) |
| 6 | 2, 5 | ceqsexv 3532 |
. 2
⊢
(∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) ∧ 𝐶 = ∪ ∪ 𝑥) ↔ 𝐶 = ∪ ∪ ({(𝐴
“ {𝐵})} ∩ Singletons )) |
| 7 | | df-apply 35874 |
. . . 4
⊢ Apply =
(( Bigcup ∘ Bigcup
) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E
↾ Singletons ) ⊗ V))) ∘
((Singleton ∘ Img) ∘ pprod( I , Singleton)))) |
| 8 | 7 | breqi 5149 |
. . 3
⊢
(〈𝐴, 𝐵〉Apply𝐶 ↔ 〈𝐴, 𝐵〉(( Bigcup
∘ Bigcup ) ∘ (((V × V)
∖ ran ((V ⊗ E ) △ (( E ↾
Singletons ) ⊗ V))) ∘ ((Singleton ∘ Img) ∘
pprod( I , Singleton))))𝐶) |
| 9 | | opex 5469 |
. . . 4
⊢
〈𝐴, 𝐵〉 ∈ V |
| 10 | | brapply.3 |
. . . 4
⊢ 𝐶 ∈ V |
| 11 | 9, 10 | brco 5881 |
. . 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 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 13 | 9, 12 | brco 5881 |
. . . . . 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 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 15 | 9, 14 | brco 5881 |
. . . . . . . . 9
⊢
(〈𝐴, 𝐵〉((Singleton ∘ Img)
∘ pprod( I , Singleton))𝑦 ↔ ∃𝑧(〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ∧ 𝑧(Singleton ∘ Img)𝑦)) |
| 16 | | brapply.1 |
. . . . . . . . . . . . 13
⊢ 𝐴 ∈ V |
| 17 | | brapply.2 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ V |
| 18 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
| 19 | 16, 17, 18 | brpprod3a 35887 |
. . . . . . . . . . . 12
⊢
(〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ↔ ∃𝑎∃𝑏(𝑧 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐵Singleton𝑏)) |
| 20 | | 3anrot 1100 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐵Singleton𝑏) ↔ (𝐴 I 𝑎 ∧ 𝐵Singleton𝑏 ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
| 21 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑎 ∈ V |
| 22 | 21 | ideq 5863 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 I 𝑎 ↔ 𝐴 = 𝑎) |
| 23 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 = 𝑎 ↔ 𝑎 = 𝐴) |
| 24 | 22, 23 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 I 𝑎 ↔ 𝑎 = 𝐴) |
| 25 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑏 ∈ V |
| 26 | 17, 25 | brsingle 35918 |
. . . . . . . . . . . . . . 15
⊢ (𝐵Singleton𝑏 ↔ 𝑏 = {𝐵}) |
| 27 | | biid 261 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑎, 𝑏〉 ↔ 𝑧 = 〈𝑎, 𝑏〉) |
| 28 | 24, 26, 27 | 3anbi123i 1156 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 I 𝑎 ∧ 𝐵Singleton𝑏 ∧ 𝑧 = 〈𝑎, 𝑏〉) ↔ (𝑎 = 𝐴 ∧ 𝑏 = {𝐵} ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
| 29 | 20, 28 | bitri 275 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐵Singleton𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = {𝐵} ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
| 30 | 29 | 2exbii 1849 |
. . . . . . . . . . . 12
⊢
(∃𝑎∃𝑏(𝑧 = 〈𝑎, 𝑏〉 ∧ 𝐴 I 𝑎 ∧ 𝐵Singleton𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = {𝐵} ∧ 𝑧 = 〈𝑎, 𝑏〉)) |
| 31 | | snex 5436 |
. . . . . . . . . . . . 13
⊢ {𝐵} ∈ V |
| 32 | | opeq1 4873 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
| 33 | 32 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → (𝑧 = 〈𝑎, 𝑏〉 ↔ 𝑧 = 〈𝐴, 𝑏〉)) |
| 34 | | opeq2 4874 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = {𝐵} → 〈𝐴, 𝑏〉 = 〈𝐴, {𝐵}〉) |
| 35 | 34 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑏 = {𝐵} → (𝑧 = 〈𝐴, 𝑏〉 ↔ 𝑧 = 〈𝐴, {𝐵}〉)) |
| 36 | 16, 31, 33, 35 | ceqsex2v 3536 |
. . . . . . . . . . . 12
⊢
(∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = {𝐵} ∧ 𝑧 = 〈𝑎, 𝑏〉) ↔ 𝑧 = 〈𝐴, {𝐵}〉) |
| 37 | 19, 30, 36 | 3bitri 297 |
. . . . . . . . . . 11
⊢
(〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ↔ 𝑧 = 〈𝐴, {𝐵}〉) |
| 38 | 37 | anbi1i 624 |
. . . . . . . . . 10
⊢
((〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ (𝑧 = 〈𝐴, {𝐵}〉 ∧ 𝑧(Singleton ∘ Img)𝑦)) |
| 39 | 38 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑧(〈𝐴, 𝐵〉pprod( I , Singleton)𝑧 ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ ∃𝑧(𝑧 = 〈𝐴, {𝐵}〉 ∧ 𝑧(Singleton ∘ Img)𝑦)) |
| 40 | | opex 5469 |
. . . . . . . . . . 11
⊢
〈𝐴, {𝐵}〉 ∈
V |
| 41 | | breq1 5146 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝐴, {𝐵}〉 → (𝑧(Singleton ∘ Img)𝑦 ↔ 〈𝐴, {𝐵}〉(Singleton ∘ Img)𝑦)) |
| 42 | 40, 41 | ceqsexv 3532 |
. . . . . . . . . 10
⊢
(∃𝑧(𝑧 = 〈𝐴, {𝐵}〉 ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ 〈𝐴, {𝐵}〉(Singleton ∘ Img)𝑦) |
| 43 | 40, 14 | brco 5881 |
. . . . . . . . . 10
⊢
(〈𝐴, {𝐵}〉(Singleton ∘
Img)𝑦 ↔ ∃𝑥(〈𝐴, {𝐵}〉Img𝑥 ∧ 𝑥Singleton𝑦)) |
| 44 | 16, 31, 12 | brimg 35938 |
. . . . . . . . . . . . 13
⊢
(〈𝐴, {𝐵}〉Img𝑥 ↔ 𝑥 = (𝐴 “ {𝐵})) |
| 45 | 12, 14 | brsingle 35918 |
. . . . . . . . . . . . 13
⊢ (𝑥Singleton𝑦 ↔ 𝑦 = {𝑥}) |
| 46 | 44, 45 | anbi12i 628 |
. . . . . . . . . . . 12
⊢
((〈𝐴, {𝐵}〉Img𝑥 ∧ 𝑥Singleton𝑦) ↔ (𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥})) |
| 47 | 46 | exbii 1848 |
. . . . . . . . . . 11
⊢
(∃𝑥(〈𝐴, {𝐵}〉Img𝑥 ∧ 𝑥Singleton𝑦) ↔ ∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥})) |
| 48 | 16 | imaex 7936 |
. . . . . . . . . . . 12
⊢ (𝐴 “ {𝐵}) ∈ V |
| 49 | | sneq 4636 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 “ {𝐵}) → {𝑥} = {(𝐴 “ {𝐵})}) |
| 50 | 49 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐴 “ {𝐵}) → (𝑦 = {𝑥} ↔ 𝑦 = {(𝐴 “ {𝐵})})) |
| 51 | 48, 50 | ceqsexv 3532 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 = (𝐴 “ {𝐵}) ∧ 𝑦 = {𝑥}) ↔ 𝑦 = {(𝐴 “ {𝐵})}) |
| 52 | 47, 51 | bitri 275 |
. . . . . . . . . 10
⊢
(∃𝑥(〈𝐴, {𝐵}〉Img𝑥 ∧ 𝑥Singleton𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})}) |
| 53 | 42, 43, 52 | 3bitri 297 |
. . . . . . . . 9
⊢
(∃𝑧(𝑧 = 〈𝐴, {𝐵}〉 ∧ 𝑧(Singleton ∘ Img)𝑦) ↔ 𝑦 = {(𝐴 “ {𝐵})}) |
| 54 | 15, 39, 53 | 3bitri 297 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉((Singleton ∘ Img)
∘ pprod( I , Singleton))𝑦 ↔ 𝑦 = {(𝐴 “ {𝐵})}) |
| 55 | | eqid 2737 |
. . . . . . . . 9
⊢ ((V
× V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) = ((V × V) ∖ ran
((V ⊗ E ) △ (( E ↾ Singletons
) ⊗ V))) |
| 56 | | brxp 5734 |
. . . . . . . . . 10
⊢ (𝑦(V × V)𝑥 ↔ (𝑦 ∈ V ∧ 𝑥 ∈ V)) |
| 57 | 14, 12, 56 | mpbir2an 711 |
. . . . . . . . 9
⊢ 𝑦(V × V)𝑥 |
| 58 | | epel 5587 |
. . . . . . . . . . 11
⊢ (𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦) |
| 59 | 58 | anbi1ci 626 |
. . . . . . . . . 10
⊢ ((𝑧 ∈
Singletons ∧ 𝑧
E 𝑦) ↔ (𝑧 ∈ 𝑦 ∧ 𝑧 ∈ Singletons
)) |
| 60 | 14 | brresi 6006 |
. . . . . . . . . 10
⊢ (𝑧( E ↾ Singletons )𝑦 ↔ (𝑧 ∈ Singletons
∧ 𝑧 E 𝑦)) |
| 61 | | elin 3967 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑦 ∩ Singletons
) ↔ (𝑧 ∈
𝑦 ∧ 𝑧 ∈ Singletons
)) |
| 62 | 59, 60, 61 | 3bitr4ri 304 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝑦 ∩ Singletons
) ↔ 𝑧( E
↾ Singletons )𝑦) |
| 63 | 14, 12, 55, 57, 62 | brtxpsd3 35897 |
. . . . . . . 8
⊢ (𝑦((V × V) ∖ ran ((V
⊗ E ) △ (( E ↾ Singletons )
⊗ V)))𝑥 ↔ 𝑥 = (𝑦 ∩ Singletons
)) |
| 64 | 54, 63 | anbi12i 628 |
. . . . . . 7
⊢
((〈𝐴, 𝐵〉((Singleton ∘ Img)
∘ pprod( I , Singleton))𝑦 ∧ 𝑦((V × V) ∖ ran ((V ⊗ E )
△ (( E ↾ Singletons ) ⊗
V)))𝑥) ↔ (𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 ∩ Singletons
))) |
| 65 | 64 | exbii 1848 |
. . . . . 6
⊢
(∃𝑦(〈𝐴, 𝐵〉((Singleton ∘ Img) ∘
pprod( I , Singleton))𝑦
∧ 𝑦((V × V)
∖ ran ((V ⊗ E ) △ (( E ↾
Singletons ) ⊗ V)))𝑥) ↔ ∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 ∩ Singletons
))) |
| 66 | | ineq1 4213 |
. . . . . . . 8
⊢ (𝑦 = {(𝐴 “ {𝐵})} → (𝑦 ∩ Singletons
) = ({(𝐴 “
{𝐵})} ∩ Singletons )) |
| 67 | 66 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = {(𝐴 “ {𝐵})} → (𝑥 = (𝑦 ∩ Singletons
) ↔ 𝑥 =
({(𝐴 “ {𝐵})} ∩
Singletons ))) |
| 68 | 1, 67 | ceqsexv 3532 |
. . . . . 6
⊢
(∃𝑦(𝑦 = {(𝐴 “ {𝐵})} ∧ 𝑥 = (𝑦 ∩ Singletons
)) ↔ 𝑥 =
({(𝐴 “ {𝐵})} ∩
Singletons )) |
| 69 | 13, 65, 68 | 3bitri 297 |
. . . . 5
⊢
(〈𝐴, 𝐵〉(((V × V) ∖
ran ((V ⊗ E ) △ (( E ↾ Singletons
) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I ,
Singleton)))𝑥 ↔ 𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
)) |
| 70 | 12, 10 | brco 5881 |
. . . . . 6
⊢ (𝑥( Bigcup
∘ Bigcup )𝐶 ↔ ∃𝑦(𝑥 Bigcup 𝑦 ∧ 𝑦 Bigcup 𝐶)) |
| 71 | 14 | brbigcup 35899 |
. . . . . . . . 9
⊢ (𝑥 Bigcup
𝑦 ↔ ∪ 𝑥 =
𝑦) |
| 72 | | eqcom 2744 |
. . . . . . . . 9
⊢ (∪ 𝑥 =
𝑦 ↔ 𝑦 = ∪ 𝑥) |
| 73 | 71, 72 | bitri 275 |
. . . . . . . 8
⊢ (𝑥 Bigcup
𝑦 ↔ 𝑦 = ∪
𝑥) |
| 74 | 10 | brbigcup 35899 |
. . . . . . . . 9
⊢ (𝑦 Bigcup
𝐶 ↔ ∪ 𝑦 =
𝐶) |
| 75 | | eqcom 2744 |
. . . . . . . . 9
⊢ (∪ 𝑦 =
𝐶 ↔ 𝐶 = ∪ 𝑦) |
| 76 | 74, 75 | bitri 275 |
. . . . . . . 8
⊢ (𝑦 Bigcup
𝐶 ↔ 𝐶 = ∪
𝑦) |
| 77 | 73, 76 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑥 Bigcup
𝑦 ∧ 𝑦 Bigcup
𝐶) ↔ (𝑦 = ∪
𝑥 ∧ 𝐶 = ∪ 𝑦)) |
| 78 | 77 | exbii 1848 |
. . . . . 6
⊢
(∃𝑦(𝑥 Bigcup
𝑦 ∧ 𝑦 Bigcup
𝐶) ↔
∃𝑦(𝑦 = ∪ 𝑥 ∧ 𝐶 = ∪ 𝑦)) |
| 79 | | vuniex 7759 |
. . . . . . 7
⊢ ∪ 𝑥
∈ V |
| 80 | | unieq 4918 |
. . . . . . . 8
⊢ (𝑦 = ∪
𝑥 → ∪ 𝑦 =
∪ ∪ 𝑥) |
| 81 | 80 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = ∪
𝑥 → (𝐶 = ∪ 𝑦 ↔ 𝐶 = ∪ ∪ 𝑥)) |
| 82 | 79, 81 | ceqsexv 3532 |
. . . . . 6
⊢
(∃𝑦(𝑦 = ∪
𝑥 ∧ 𝐶 = ∪ 𝑦) ↔ 𝐶 = ∪ ∪ 𝑥) |
| 83 | 70, 78, 82 | 3bitri 297 |
. . . . 5
⊢ (𝑥( Bigcup
∘ Bigcup )𝐶 ↔ 𝐶 = ∪ ∪ 𝑥) |
| 84 | 69, 83 | anbi12i 628 |
. . . 4
⊢
((〈𝐴, 𝐵〉(((V × V) ∖
ran ((V ⊗ E ) △ (( E ↾ Singletons
) ⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I ,
Singleton)))𝑥 ∧ 𝑥( Bigcup
∘ Bigcup )𝐶) ↔ (𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) ∧ 𝐶 = ∪ ∪ 𝑥)) |
| 85 | 84 | exbii 1848 |
. . 3
⊢
(∃𝑥(〈𝐴, 𝐵〉(((V × V) ∖ ran ((V
⊗ E ) △ (( E ↾ Singletons )
⊗ V))) ∘ ((Singleton ∘ Img) ∘ pprod( I ,
Singleton)))𝑥 ∧ 𝑥( Bigcup
∘ Bigcup )𝐶) ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) ∧ 𝐶 = ∪ ∪ 𝑥)) |
| 86 | 8, 11, 85 | 3bitri 297 |
. 2
⊢
(〈𝐴, 𝐵〉Apply𝐶 ↔ ∃𝑥(𝑥 = ({(𝐴 “ {𝐵})} ∩ Singletons
) ∧ 𝐶 = ∪ ∪ 𝑥)) |
| 87 | | dffv5 35925 |
. . 3
⊢ (𝐴‘𝐵) = ∪ ∪ ({(𝐴
“ {𝐵})} ∩ Singletons ) |
| 88 | 87 | eqeq2i 2750 |
. 2
⊢ (𝐶 = (𝐴‘𝐵) ↔ 𝐶 = ∪ ∪ ({(𝐴
“ {𝐵})} ∩ Singletons )) |
| 89 | 6, 86, 88 | 3bitr4i 303 |
1
⊢
(〈𝐴, 𝐵〉Apply𝐶 ↔ 𝐶 = (𝐴‘𝐵)) |