Step | Hyp | Ref
| Expression |
1 | | snex 5432 |
. . . 4
β’ {(π΄ β {π΅})} β V |
2 | 1 | inex1 5318 |
. . 3
β’ ({(π΄ β {π΅})} β© Singletons
) β V |
3 | | unieq 4920 |
. . . . 5
β’ (π₯ = ({(π΄ β {π΅})} β© Singletons
) β βͺ π₯ = βͺ ({(π΄ β {π΅})} β© Singletons
)) |
4 | 3 | unieqd 4923 |
. . . 4
β’ (π₯ = ({(π΄ β {π΅})} β© Singletons
) β βͺ βͺ π₯ = βͺ
βͺ ({(π΄ β {π΅})} β© Singletons
)) |
5 | 4 | eqeq2d 2744 |
. . 3
β’ (π₯ = ({(π΄ β {π΅})} β© Singletons
) β (πΆ = βͺ βͺ π₯ β πΆ = βͺ βͺ ({(π΄
β {π΅})} β© Singletons ))) |
6 | 2, 5 | ceqsexv 3526 |
. 2
β’
(βπ₯(π₯ = ({(π΄ β {π΅})} β© Singletons
) β§ πΆ = βͺ βͺ π₯) β πΆ = βͺ βͺ ({(π΄
β {π΅})} β© Singletons )) |
7 | | df-apply 34845 |
. . . 4
β’ Apply =
(( Bigcup β Bigcup
) β (((V Γ V) β ran ((V β E ) β³ (( E
βΎ Singletons ) β V))) β
((Singleton β Img) β pprod( I , Singleton)))) |
8 | 7 | breqi 5155 |
. . 3
β’
(β¨π΄, π΅β©ApplyπΆ β β¨π΄, π΅β©(( Bigcup
β Bigcup ) β (((V Γ V)
β ran ((V β E ) β³ (( E βΎ
Singletons ) β V))) β ((Singleton β Img) β
pprod( I , Singleton))))πΆ) |
9 | | opex 5465 |
. . . 4
β’
β¨π΄, π΅β© β V |
10 | | brapply.3 |
. . . 4
β’ πΆ β V |
11 | 9, 10 | brco 5871 |
. . 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 3479 |
. . . . . . 7
β’ π₯ β V |
13 | 9, 12 | brco 5871 |
. . . . . 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 3479 |
. . . . . . . . . 10
β’ π¦ β V |
15 | 9, 14 | brco 5871 |
. . . . . . . . 9
β’
(β¨π΄, π΅β©((Singleton β Img)
β pprod( I , Singleton))π¦ β βπ§(β¨π΄, π΅β©pprod( I , Singleton)π§ β§ π§(Singleton β Img)π¦)) |
16 | | brapply.1 |
. . . . . . . . . . . . 13
β’ π΄ β V |
17 | | brapply.2 |
. . . . . . . . . . . . 13
β’ π΅ β V |
18 | | vex 3479 |
. . . . . . . . . . . . 13
β’ π§ β V |
19 | 16, 17, 18 | brpprod3a 34858 |
. . . . . . . . . . . 12
β’
(β¨π΄, π΅β©pprod( I , Singleton)π§ β βπβπ(π§ = β¨π, πβ© β§ π΄ I π β§ π΅Singletonπ)) |
20 | | 3anrot 1101 |
. . . . . . . . . . . . . 14
β’ ((π§ = β¨π, πβ© β§ π΄ I π β§ π΅Singletonπ) β (π΄ I π β§ π΅Singletonπ β§ π§ = β¨π, πβ©)) |
21 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
22 | 21 | ideq 5853 |
. . . . . . . . . . . . . . . 16
β’ (π΄ I π β π΄ = π) |
23 | | eqcom 2740 |
. . . . . . . . . . . . . . . 16
β’ (π΄ = π β π = π΄) |
24 | 22, 23 | bitri 275 |
. . . . . . . . . . . . . . 15
β’ (π΄ I π β π = π΄) |
25 | | vex 3479 |
. . . . . . . . . . . . . . . 16
β’ π β V |
26 | 17, 25 | brsingle 34889 |
. . . . . . . . . . . . . . 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 1852 |
. . . . . . . . . . . 12
β’
(βπβπ(π§ = β¨π, πβ© β§ π΄ I π β§ π΅Singletonπ) β βπβπ(π = π΄ β§ π = {π΅} β§ π§ = β¨π, πβ©)) |
31 | | snex 5432 |
. . . . . . . . . . . . 13
β’ {π΅} β V |
32 | | opeq1 4874 |
. . . . . . . . . . . . . 14
β’ (π = π΄ β β¨π, πβ© = β¨π΄, πβ©) |
33 | 32 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π = π΄ β (π§ = β¨π, πβ© β π§ = β¨π΄, πβ©)) |
34 | | opeq2 4875 |
. . . . . . . . . . . . . 14
β’ (π = {π΅} β β¨π΄, πβ© = β¨π΄, {π΅}β©) |
35 | 34 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π = {π΅} β (π§ = β¨π΄, πβ© β π§ = β¨π΄, {π΅}β©)) |
36 | 16, 31, 33, 35 | ceqsex2v 3531 |
. . . . . . . . . . . 12
β’
(βπβπ(π = π΄ β§ π = {π΅} β§ π§ = β¨π, πβ©) β π§ = β¨π΄, {π΅}β©) |
37 | 19, 30, 36 | 3bitri 297 |
. . . . . . . . . . 11
β’
(β¨π΄, π΅β©pprod( I , Singleton)π§ β π§ = β¨π΄, {π΅}β©) |
38 | 37 | anbi1i 625 |
. . . . . . . . . 10
β’
((β¨π΄, π΅β©pprod( I , Singleton)π§ β§ π§(Singleton β Img)π¦) β (π§ = β¨π΄, {π΅}β© β§ π§(Singleton β Img)π¦)) |
39 | 38 | exbii 1851 |
. . . . . . . . 9
β’
(βπ§(β¨π΄, π΅β©pprod( I , Singleton)π§ β§ π§(Singleton β Img)π¦) β βπ§(π§ = β¨π΄, {π΅}β© β§ π§(Singleton β Img)π¦)) |
40 | | opex 5465 |
. . . . . . . . . . 11
β’
β¨π΄, {π΅}β© β
V |
41 | | breq1 5152 |
. . . . . . . . . . 11
β’ (π§ = β¨π΄, {π΅}β© β (π§(Singleton β Img)π¦ β β¨π΄, {π΅}β©(Singleton β Img)π¦)) |
42 | 40, 41 | ceqsexv 3526 |
. . . . . . . . . 10
β’
(βπ§(π§ = β¨π΄, {π΅}β© β§ π§(Singleton β Img)π¦) β β¨π΄, {π΅}β©(Singleton β Img)π¦) |
43 | 40, 14 | brco 5871 |
. . . . . . . . . 10
β’
(β¨π΄, {π΅}β©(Singleton β
Img)π¦ β βπ₯(β¨π΄, {π΅}β©Imgπ₯ β§ π₯Singletonπ¦)) |
44 | 16, 31, 12 | brimg 34909 |
. . . . . . . . . . . . 13
β’
(β¨π΄, {π΅}β©Imgπ₯ β π₯ = (π΄ β {π΅})) |
45 | 12, 14 | brsingle 34889 |
. . . . . . . . . . . . 13
β’ (π₯Singletonπ¦ β π¦ = {π₯}) |
46 | 44, 45 | anbi12i 628 |
. . . . . . . . . . . 12
β’
((β¨π΄, {π΅}β©Imgπ₯ β§ π₯Singletonπ¦) β (π₯ = (π΄ β {π΅}) β§ π¦ = {π₯})) |
47 | 46 | exbii 1851 |
. . . . . . . . . . 11
β’
(βπ₯(β¨π΄, {π΅}β©Imgπ₯ β§ π₯Singletonπ¦) β βπ₯(π₯ = (π΄ β {π΅}) β§ π¦ = {π₯})) |
48 | 16 | imaex 7907 |
. . . . . . . . . . . 12
β’ (π΄ β {π΅}) β V |
49 | | sneq 4639 |
. . . . . . . . . . . . 13
β’ (π₯ = (π΄ β {π΅}) β {π₯} = {(π΄ β {π΅})}) |
50 | 49 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π₯ = (π΄ β {π΅}) β (π¦ = {π₯} β π¦ = {(π΄ β {π΅})})) |
51 | 48, 50 | ceqsexv 3526 |
. . . . . . . . . . 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 2733 |
. . . . . . . . 9
β’ ((V
Γ V) β ran ((V β E ) β³ (( E βΎ Singletons ) β V))) = ((V Γ V) β ran
((V β E ) β³ (( E βΎ Singletons
) β V))) |
56 | | brxp 5726 |
. . . . . . . . . 10
β’ (π¦(V Γ V)π₯ β (π¦ β V β§ π₯ β V)) |
57 | 14, 12, 56 | mpbir2an 710 |
. . . . . . . . 9
β’ π¦(V Γ V)π₯ |
58 | | epel 5584 |
. . . . . . . . . . 11
β’ (π§ E π¦ β π§ β π¦) |
59 | 58 | anbi1ci 627 |
. . . . . . . . . 10
β’ ((π§ β
Singletons β§ π§
E π¦) β (π§ β π¦ β§ π§ β Singletons
)) |
60 | 14 | brresi 5991 |
. . . . . . . . . 10
β’ (π§( E βΎ Singletons )π¦ β (π§ β Singletons
β§ π§ E π¦)) |
61 | | elin 3965 |
. . . . . . . . . 10
β’ (π§ β (π¦ β© Singletons
) β (π§ β
π¦ β§ π§ β Singletons
)) |
62 | 59, 60, 61 | 3bitr4ri 304 |
. . . . . . . . 9
β’ (π§ β (π¦ β© Singletons
) β π§( E
βΎ Singletons )π¦) |
63 | 14, 12, 55, 57, 62 | brtxpsd3 34868 |
. . . . . . . 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 1851 |
. . . . . 6
β’
(βπ¦(β¨π΄, π΅β©((Singleton β Img) β
pprod( I , Singleton))π¦
β§ π¦((V Γ V)
β ran ((V β E ) β³ (( E βΎ
Singletons ) β V)))π₯) β βπ¦(π¦ = {(π΄ β {π΅})} β§ π₯ = (π¦ β© Singletons
))) |
66 | | ineq1 4206 |
. . . . . . . 8
β’ (π¦ = {(π΄ β {π΅})} β (π¦ β© Singletons
) = ({(π΄ β
{π΅})} β© Singletons )) |
67 | 66 | eqeq2d 2744 |
. . . . . . 7
β’ (π¦ = {(π΄ β {π΅})} β (π₯ = (π¦ β© Singletons
) β π₯ =
({(π΄ β {π΅})} β©
Singletons ))) |
68 | 1, 67 | ceqsexv 3526 |
. . . . . 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 5871 |
. . . . . 6
β’ (π₯( Bigcup
β Bigcup )πΆ β βπ¦(π₯ Bigcup π¦ β§ π¦ Bigcup πΆ)) |
71 | 14 | brbigcup 34870 |
. . . . . . . . 9
β’ (π₯ Bigcup
π¦ β βͺ π₯ =
π¦) |
72 | | eqcom 2740 |
. . . . . . . . 9
β’ (βͺ π₯ =
π¦ β π¦ = βͺ π₯) |
73 | 71, 72 | bitri 275 |
. . . . . . . 8
β’ (π₯ Bigcup
π¦ β π¦ = βͺ
π₯) |
74 | 10 | brbigcup 34870 |
. . . . . . . . 9
β’ (π¦ Bigcup
πΆ β βͺ π¦ =
πΆ) |
75 | | eqcom 2740 |
. . . . . . . . 9
β’ (βͺ π¦ =
πΆ β πΆ = βͺ π¦) |
76 | 74, 75 | bitri 275 |
. . . . . . . 8
β’ (π¦ Bigcup
πΆ β πΆ = βͺ
π¦) |
77 | 73, 76 | anbi12i 628 |
. . . . . . 7
β’ ((π₯ Bigcup
π¦ β§ π¦ Bigcup
πΆ) β (π¦ = βͺ
π₯ β§ πΆ = βͺ π¦)) |
78 | 77 | exbii 1851 |
. . . . . 6
β’
(βπ¦(π₯ Bigcup
π¦ β§ π¦ Bigcup
πΆ) β
βπ¦(π¦ = βͺ π₯ β§ πΆ = βͺ π¦)) |
79 | | vuniex 7729 |
. . . . . . 7
β’ βͺ π₯
β V |
80 | | unieq 4920 |
. . . . . . . 8
β’ (π¦ = βͺ
π₯ β βͺ π¦ =
βͺ βͺ π₯) |
81 | 80 | eqeq2d 2744 |
. . . . . . 7
β’ (π¦ = βͺ
π₯ β (πΆ = βͺ π¦ β πΆ = βͺ βͺ π₯)) |
82 | 79, 81 | ceqsexv 3526 |
. . . . . 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 1851 |
. . 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 34896 |
. . 3
β’ (π΄βπ΅) = βͺ βͺ ({(π΄
β {π΅})} β© Singletons ) |
88 | 87 | eqeq2i 2746 |
. 2
β’ (πΆ = (π΄βπ΅) β πΆ = βͺ βͺ ({(π΄
β {π΅})} β© Singletons )) |
89 | 6, 86, 88 | 3bitr4i 303 |
1
β’
(β¨π΄, π΅β©ApplyπΆ β πΆ = (π΄βπ΅)) |