Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . 4
β’
(2nd β(πβ(π΄βπ))) β V |
2 | | axcc2lem.3 |
. . . 4
β’ πΊ = (π β Ο β¦ (2nd
β(πβ(π΄βπ)))) |
3 | 1, 2 | fnmpti 6645 |
. . 3
β’ πΊ Fn Ο |
4 | | vsnex 5387 |
. . . . . . . . . . . . . . 15
β’ {π} β V |
5 | | fvex 6856 |
. . . . . . . . . . . . . . 15
β’ (πΎβπ) β V |
6 | 4, 5 | xpex 7688 |
. . . . . . . . . . . . . 14
β’ ({π} Γ (πΎβπ)) β V |
7 | | axcc2lem.2 |
. . . . . . . . . . . . . . 15
β’ π΄ = (π β Ο β¦ ({π} Γ (πΎβπ))) |
8 | 7 | fvmpt2 6960 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ ({π} Γ (πΎβπ)) β V) β (π΄βπ) = ({π} Γ (πΎβπ))) |
9 | 6, 8 | mpan2 690 |
. . . . . . . . . . . . 13
β’ (π β Ο β (π΄βπ) = ({π} Γ (πΎβπ))) |
10 | | vex 3450 |
. . . . . . . . . . . . . . 15
β’ π β V |
11 | 10 | snnz 4738 |
. . . . . . . . . . . . . 14
β’ {π} β β
|
12 | | 0ex 5265 |
. . . . . . . . . . . . . . . . . 18
β’ β
β V |
13 | 12 | snnz 4738 |
. . . . . . . . . . . . . . . . 17
β’ {β
}
β β
|
14 | | iftrue 4493 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) = β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) = {β
}) |
15 | 14 | neeq1d 3004 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) = β
β (if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
β {β
} β
β
)) |
16 | 13, 15 | mpbiri 258 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) = β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
) |
17 | | iffalse 4496 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
(πΉβπ) = β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) = (πΉβπ)) |
18 | | neqne 2952 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
(πΉβπ) = β
β (πΉβπ) β β
) |
19 | 17, 18 | eqnetrd 3012 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(πΉβπ) = β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
) |
20 | 16, 19 | pm2.61i 182 |
. . . . . . . . . . . . . . 15
β’ if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
|
21 | | p0ex 5340 |
. . . . . . . . . . . . . . . . . 18
β’ {β
}
β V |
22 | | fvex 6856 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉβπ) β V |
23 | 21, 22 | ifex 4537 |
. . . . . . . . . . . . . . . . 17
β’ if((πΉβπ) = β
, {β
}, (πΉβπ)) β V |
24 | | axcc2lem.1 |
. . . . . . . . . . . . . . . . . 18
β’ πΎ = (π β Ο β¦ if((πΉβπ) = β
, {β
}, (πΉβπ))) |
25 | 24 | fvmpt2 6960 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ if((πΉβπ) = β
, {β
}, (πΉβπ)) β V) β (πΎβπ) = if((πΉβπ) = β
, {β
}, (πΉβπ))) |
26 | 23, 25 | mpan2 690 |
. . . . . . . . . . . . . . . 16
β’ (π β Ο β (πΎβπ) = if((πΉβπ) = β
, {β
}, (πΉβπ))) |
27 | 26 | neeq1d 3004 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β ((πΎβπ) β β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
)) |
28 | 20, 27 | mpbiri 258 |
. . . . . . . . . . . . . 14
β’ (π β Ο β (πΎβπ) β β
) |
29 | | xpnz 6112 |
. . . . . . . . . . . . . . 15
β’ (({π} β β
β§ (πΎβπ) β β
) β ({π} Γ (πΎβπ)) β β
) |
30 | 29 | biimpi 215 |
. . . . . . . . . . . . . 14
β’ (({π} β β
β§ (πΎβπ) β β
) β ({π} Γ (πΎβπ)) β β
) |
31 | 11, 28, 30 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π β Ο β ({π} Γ (πΎβπ)) β β
) |
32 | 9, 31 | eqnetrd 3012 |
. . . . . . . . . . . 12
β’ (π β Ο β (π΄βπ) β β
) |
33 | 6, 7 | fnmpti 6645 |
. . . . . . . . . . . . . 14
β’ π΄ Fn Ο |
34 | | fnfvelrn 7032 |
. . . . . . . . . . . . . 14
β’ ((π΄ Fn Ο β§ π β Ο) β (π΄βπ) β ran π΄) |
35 | 33, 34 | mpan 689 |
. . . . . . . . . . . . 13
β’ (π β Ο β (π΄βπ) β ran π΄) |
36 | | neeq1 3007 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π΄βπ) β (π§ β β
β (π΄βπ) β β
)) |
37 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π΄βπ) β (πβπ§) = (πβ(π΄βπ))) |
38 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π΄βπ) β π§ = (π΄βπ)) |
39 | 37, 38 | eleq12d 2832 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π΄βπ) β ((πβπ§) β π§ β (πβ(π΄βπ)) β (π΄βπ))) |
40 | 36, 39 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π§ = (π΄βπ) β ((π§ β β
β (πβπ§) β π§) β ((π΄βπ) β β
β (πβ(π΄βπ)) β (π΄βπ)))) |
41 | 40 | rspccv 3579 |
. . . . . . . . . . . . 13
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β ((π΄βπ) β ran π΄ β ((π΄βπ) β β
β (πβ(π΄βπ)) β (π΄βπ)))) |
42 | 35, 41 | syl5 34 |
. . . . . . . . . . . 12
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β (π β Ο β ((π΄βπ) β β
β (πβ(π΄βπ)) β (π΄βπ)))) |
43 | 32, 42 | mpdi 45 |
. . . . . . . . . . 11
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β (π β Ο β (πβ(π΄βπ)) β (π΄βπ))) |
44 | 43 | impcom 409 |
. . . . . . . . . 10
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β (πβ(π΄βπ)) β (π΄βπ)) |
45 | 9 | eleq2d 2824 |
. . . . . . . . . . 11
β’ (π β Ο β ((πβ(π΄βπ)) β (π΄βπ) β (πβ(π΄βπ)) β ({π} Γ (πΎβπ)))) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β ((πβ(π΄βπ)) β (π΄βπ) β (πβ(π΄βπ)) β ({π} Γ (πΎβπ)))) |
47 | 44, 46 | mpbid 231 |
. . . . . . . . 9
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β (πβ(π΄βπ)) β ({π} Γ (πΎβπ))) |
48 | | xp2nd 7955 |
. . . . . . . . 9
β’ ((πβ(π΄βπ)) β ({π} Γ (πΎβπ)) β (2nd β(πβ(π΄βπ))) β (πΎβπ)) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β (2nd β(πβ(π΄βπ))) β (πΎβπ)) |
50 | 49 | 3adant3 1133 |
. . . . . . 7
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (2nd
β(πβ(π΄βπ))) β (πΎβπ)) |
51 | 2 | fvmpt2 6960 |
. . . . . . . . . 10
β’ ((π β Ο β§
(2nd β(πβ(π΄βπ))) β V) β (πΊβπ) = (2nd β(πβ(π΄βπ)))) |
52 | 1, 51 | mpan2 690 |
. . . . . . . . 9
β’ (π β Ο β (πΊβπ) = (2nd β(πβ(π΄βπ)))) |
53 | 52 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (πΊβπ) = (2nd β(πβ(π΄βπ)))) |
54 | 53 | eqcomd 2743 |
. . . . . . 7
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (2nd
β(πβ(π΄βπ))) = (πΊβπ)) |
55 | 26 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (πΎβπ) = if((πΉβπ) = β
, {β
}, (πΉβπ))) |
56 | | ifnefalse 4499 |
. . . . . . . . 9
β’ ((πΉβπ) β β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) = (πΉβπ)) |
57 | 56 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β if((πΉβπ) = β
, {β
}, (πΉβπ)) = (πΉβπ)) |
58 | 55, 57 | eqtrd 2777 |
. . . . . . 7
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (πΎβπ) = (πΉβπ)) |
59 | 50, 54, 58 | 3eltr3d 2852 |
. . . . . 6
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (πΊβπ) β (πΉβπ)) |
60 | 59 | 3expia 1122 |
. . . . 5
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β ((πΉβπ) β β
β (πΊβπ) β (πΉβπ))) |
61 | 60 | expcom 415 |
. . . 4
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β (π β Ο β ((πΉβπ) β β
β (πΊβπ) β (πΉβπ)))) |
62 | 61 | ralrimiv 3143 |
. . 3
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β βπ β Ο ((πΉβπ) β β
β (πΊβπ) β (πΉβπ))) |
63 | | omex 9580 |
. . . . 5
β’ Ο
β V |
64 | | fnex 7168 |
. . . . 5
β’ ((πΊ Fn Ο β§ Ο β
V) β πΊ β
V) |
65 | 3, 63, 64 | mp2an 691 |
. . . 4
β’ πΊ β V |
66 | | fneq1 6594 |
. . . . 5
β’ (π = πΊ β (π Fn Ο β πΊ Fn Ο)) |
67 | | fveq1 6842 |
. . . . . . . 8
β’ (π = πΊ β (πβπ) = (πΊβπ)) |
68 | 67 | eleq1d 2823 |
. . . . . . 7
β’ (π = πΊ β ((πβπ) β (πΉβπ) β (πΊβπ) β (πΉβπ))) |
69 | 68 | imbi2d 341 |
. . . . . 6
β’ (π = πΊ β (((πΉβπ) β β
β (πβπ) β (πΉβπ)) β ((πΉβπ) β β
β (πΊβπ) β (πΉβπ)))) |
70 | 69 | ralbidv 3175 |
. . . . 5
β’ (π = πΊ β (βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ)) β βπ β Ο ((πΉβπ) β β
β (πΊβπ) β (πΉβπ)))) |
71 | 66, 70 | anbi12d 632 |
. . . 4
β’ (π = πΊ β ((π Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ))) β (πΊ Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πΊβπ) β (πΉβπ))))) |
72 | 65, 71 | spcev 3566 |
. . 3
β’ ((πΊ Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πΊβπ) β (πΉβπ))) β βπ(π Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ)))) |
73 | 3, 62, 72 | sylancr 588 |
. 2
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β βπ(π Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ)))) |
74 | 6 | a1i 11 |
. . . . . 6
β’ ((Ο
β V β§ π β
Ο) β ({π}
Γ (πΎβπ)) β V) |
75 | 74, 7 | fmptd 7063 |
. . . . 5
β’ (Ο
β V β π΄:ΟβΆV) |
76 | 63, 75 | ax-mp 5 |
. . . 4
β’ π΄:ΟβΆV |
77 | | sneq 4597 |
. . . . . . . . . 10
β’ (π = π β {π} = {π}) |
78 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πΎβπ) = (πΎβπ)) |
79 | 77, 78 | xpeq12d 5665 |
. . . . . . . . 9
β’ (π = π β ({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ))) |
80 | 79, 7, 6 | fvmpt3i 6954 |
. . . . . . . 8
β’ (π β Ο β (π΄βπ) = ({π} Γ (πΎβπ))) |
81 | 80 | adantl 483 |
. . . . . . 7
β’ ((π β Ο β§ π β Ο) β (π΄βπ) = ({π} Γ (πΎβπ))) |
82 | 81 | eqeq2d 2748 |
. . . . . 6
β’ ((π β Ο β§ π β Ο) β ((π΄βπ) = (π΄βπ) β (π΄βπ) = ({π} Γ (πΎβπ)))) |
83 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π β Ο β§ π β Ο) β (π΄βπ) = ({π} Γ (πΎβπ))) |
84 | 83 | eqeq1d 2739 |
. . . . . . 7
β’ ((π β Ο β§ π β Ο) β ((π΄βπ) = ({π} Γ (πΎβπ)) β ({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)))) |
85 | | xp11 6128 |
. . . . . . . . . 10
β’ (({π} β β
β§ (πΎβπ) β β
) β (({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)) β ({π} = {π} β§ (πΎβπ) = (πΎβπ)))) |
86 | 11, 28, 85 | sylancr 588 |
. . . . . . . . 9
β’ (π β Ο β (({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)) β ({π} = {π} β§ (πΎβπ) = (πΎβπ)))) |
87 | 10 | sneqr 4799 |
. . . . . . . . . 10
β’ ({π} = {π} β π = π) |
88 | 87 | adantr 482 |
. . . . . . . . 9
β’ (({π} = {π} β§ (πΎβπ) = (πΎβπ)) β π = π) |
89 | 86, 88 | syl6bi 253 |
. . . . . . . 8
β’ (π β Ο β (({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)) β π = π)) |
90 | 89 | adantr 482 |
. . . . . . 7
β’ ((π β Ο β§ π β Ο) β (({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)) β π = π)) |
91 | 84, 90 | sylbid 239 |
. . . . . 6
β’ ((π β Ο β§ π β Ο) β ((π΄βπ) = ({π} Γ (πΎβπ)) β π = π)) |
92 | 82, 91 | sylbid 239 |
. . . . 5
β’ ((π β Ο β§ π β Ο) β ((π΄βπ) = (π΄βπ) β π = π)) |
93 | 92 | rgen2 3195 |
. . . 4
β’
βπ β
Ο βπ β
Ο ((π΄βπ) = (π΄βπ) β π = π) |
94 | | dff13 7203 |
. . . 4
β’ (π΄:Οβ1-1βV β (π΄:ΟβΆV β§ βπ β Ο βπ β Ο ((π΄βπ) = (π΄βπ) β π = π))) |
95 | 76, 93, 94 | mpbir2an 710 |
. . 3
β’ π΄:Οβ1-1βV |
96 | | f1f1orn 6796 |
. . . 4
β’ (π΄:Οβ1-1βV β π΄:Οβ1-1-ontoβran
π΄) |
97 | 63 | f1oen 8914 |
. . . 4
β’ (π΄:Οβ1-1-ontoβran
π΄ β Ο β
ran π΄) |
98 | | ensym 8944 |
. . . 4
β’ (Ο
β ran π΄ β ran
π΄ β
Ο) |
99 | 96, 97, 98 | 3syl 18 |
. . 3
β’ (π΄:Οβ1-1βV β ran π΄ β Ο) |
100 | 7 | rneqi 5893 |
. . . . 5
β’ ran π΄ = ran (π β Ο β¦ ({π} Γ (πΎβπ))) |
101 | | dmmptg 6195 |
. . . . . . . 8
β’
(βπ β
Ο ({π} Γ (πΎβπ)) β V β dom (π β Ο β¦ ({π} Γ (πΎβπ))) = Ο) |
102 | 6 | a1i 11 |
. . . . . . . 8
β’ (π β Ο β ({π} Γ (πΎβπ)) β V) |
103 | 101, 102 | mprg 3071 |
. . . . . . 7
β’ dom
(π β Ο β¦
({π} Γ (πΎβπ))) = Ο |
104 | 103, 63 | eqeltri 2834 |
. . . . . 6
β’ dom
(π β Ο β¦
({π} Γ (πΎβπ))) β V |
105 | | funmpt 6540 |
. . . . . 6
β’ Fun
(π β Ο β¦
({π} Γ (πΎβπ))) |
106 | | funrnex 7887 |
. . . . . 6
β’ (dom
(π β Ο β¦
({π} Γ (πΎβπ))) β V β (Fun (π β Ο β¦ ({π} Γ (πΎβπ))) β ran (π β Ο β¦ ({π} Γ (πΎβπ))) β V)) |
107 | 104, 105,
106 | mp2 9 |
. . . . 5
β’ ran
(π β Ο β¦
({π} Γ (πΎβπ))) β V |
108 | 100, 107 | eqeltri 2834 |
. . . 4
β’ ran π΄ β V |
109 | | breq1 5109 |
. . . . 5
β’ (π = ran π΄ β (π β Ο β ran π΄ β Ο)) |
110 | | raleq 3310 |
. . . . . 6
β’ (π = ran π΄ β (βπ§ β π (π§ β β
β (πβπ§) β π§) β βπ§ β ran π΄(π§ β β
β (πβπ§) β π§))) |
111 | 110 | exbidv 1925 |
. . . . 5
β’ (π = ran π΄ β (βπβπ§ β π (π§ β β
β (πβπ§) β π§) β βπβπ§ β ran π΄(π§ β β
β (πβπ§) β π§))) |
112 | 109, 111 | imbi12d 345 |
. . . 4
β’ (π = ran π΄ β ((π β Ο β βπβπ§ β π (π§ β β
β (πβπ§) β π§)) β (ran π΄ β Ο β βπβπ§ β ran π΄(π§ β β
β (πβπ§) β π§)))) |
113 | | ax-cc 10372 |
. . . 4
β’ (π β Ο β
βπβπ§ β π (π§ β β
β (πβπ§) β π§)) |
114 | 108, 112,
113 | vtocl 3519 |
. . 3
β’ (ran
π΄ β Ο β
βπβπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) |
115 | 95, 99, 114 | mp2b 10 |
. 2
β’
βπβπ§ β ran π΄(π§ β β
β (πβπ§) β π§) |
116 | 73, 115 | exlimiiv 1935 |
1
β’
βπ(π Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ))) |