Step | Hyp | Ref
| Expression |
1 | | fvex 6904 |
. . . 4
β’
(2nd β(πβ(π΄βπ))) β V |
2 | | axcc2lem.3 |
. . . 4
β’ πΊ = (π β Ο β¦ (2nd
β(πβ(π΄βπ)))) |
3 | 1, 2 | fnmpti 6693 |
. . 3
β’ πΊ Fn Ο |
4 | | vsnex 5429 |
. . . . . . . . . . . . . . 15
β’ {π} β V |
5 | | fvex 6904 |
. . . . . . . . . . . . . . 15
β’ (πΎβπ) β V |
6 | 4, 5 | xpex 7742 |
. . . . . . . . . . . . . 14
β’ ({π} Γ (πΎβπ)) β V |
7 | | axcc2lem.2 |
. . . . . . . . . . . . . . 15
β’ π΄ = (π β Ο β¦ ({π} Γ (πΎβπ))) |
8 | 7 | fvmpt2 7009 |
. . . . . . . . . . . . . 14
β’ ((π β Ο β§ ({π} Γ (πΎβπ)) β V) β (π΄βπ) = ({π} Γ (πΎβπ))) |
9 | 6, 8 | mpan2 689 |
. . . . . . . . . . . . 13
β’ (π β Ο β (π΄βπ) = ({π} Γ (πΎβπ))) |
10 | | vex 3478 |
. . . . . . . . . . . . . . 15
β’ π β V |
11 | 10 | snnz 4780 |
. . . . . . . . . . . . . 14
β’ {π} β β
|
12 | | 0ex 5307 |
. . . . . . . . . . . . . . . . . 18
β’ β
β V |
13 | 12 | snnz 4780 |
. . . . . . . . . . . . . . . . 17
β’ {β
}
β β
|
14 | | iftrue 4534 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ) = β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) = {β
}) |
15 | 14 | neeq1d 3000 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ) = β
β (if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
β {β
} β
β
)) |
16 | 13, 15 | mpbiri 257 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) = β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
) |
17 | | iffalse 4537 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
(πΉβπ) = β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) = (πΉβπ)) |
18 | | neqne 2948 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
(πΉβπ) = β
β (πΉβπ) β β
) |
19 | 17, 18 | eqnetrd 3008 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(πΉβπ) = β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
) |
20 | 16, 19 | pm2.61i 182 |
. . . . . . . . . . . . . . 15
β’ if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
|
21 | | p0ex 5382 |
. . . . . . . . . . . . . . . . . 18
β’ {β
}
β V |
22 | | fvex 6904 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉβπ) β V |
23 | 21, 22 | ifex 4578 |
. . . . . . . . . . . . . . . . 17
β’ if((πΉβπ) = β
, {β
}, (πΉβπ)) β V |
24 | | axcc2lem.1 |
. . . . . . . . . . . . . . . . . 18
β’ πΎ = (π β Ο β¦ if((πΉβπ) = β
, {β
}, (πΉβπ))) |
25 | 24 | fvmpt2 7009 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Ο β§ if((πΉβπ) = β
, {β
}, (πΉβπ)) β V) β (πΎβπ) = if((πΉβπ) = β
, {β
}, (πΉβπ))) |
26 | 23, 25 | mpan2 689 |
. . . . . . . . . . . . . . . 16
β’ (π β Ο β (πΎβπ) = if((πΉβπ) = β
, {β
}, (πΉβπ))) |
27 | 26 | neeq1d 3000 |
. . . . . . . . . . . . . . 15
β’ (π β Ο β ((πΎβπ) β β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) β β
)) |
28 | 20, 27 | mpbiri 257 |
. . . . . . . . . . . . . 14
β’ (π β Ο β (πΎβπ) β β
) |
29 | | xpnz 6158 |
. . . . . . . . . . . . . . 15
β’ (({π} β β
β§ (πΎβπ) β β
) β ({π} Γ (πΎβπ)) β β
) |
30 | 29 | biimpi 215 |
. . . . . . . . . . . . . 14
β’ (({π} β β
β§ (πΎβπ) β β
) β ({π} Γ (πΎβπ)) β β
) |
31 | 11, 28, 30 | sylancr 587 |
. . . . . . . . . . . . 13
β’ (π β Ο β ({π} Γ (πΎβπ)) β β
) |
32 | 9, 31 | eqnetrd 3008 |
. . . . . . . . . . . 12
β’ (π β Ο β (π΄βπ) β β
) |
33 | 6, 7 | fnmpti 6693 |
. . . . . . . . . . . . . 14
β’ π΄ Fn Ο |
34 | | fnfvelrn 7082 |
. . . . . . . . . . . . . 14
β’ ((π΄ Fn Ο β§ π β Ο) β (π΄βπ) β ran π΄) |
35 | 33, 34 | mpan 688 |
. . . . . . . . . . . . 13
β’ (π β Ο β (π΄βπ) β ran π΄) |
36 | | neeq1 3003 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π΄βπ) β (π§ β β
β (π΄βπ) β β
)) |
37 | | fveq2 6891 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π΄βπ) β (πβπ§) = (πβ(π΄βπ))) |
38 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π§ = (π΄βπ) β π§ = (π΄βπ)) |
39 | 37, 38 | eleq12d 2827 |
. . . . . . . . . . . . . . 15
β’ (π§ = (π΄βπ) β ((πβπ§) β π§ β (πβ(π΄βπ)) β (π΄βπ))) |
40 | 36, 39 | imbi12d 344 |
. . . . . . . . . . . . . 14
β’ (π§ = (π΄βπ) β ((π§ β β
β (πβπ§) β π§) β ((π΄βπ) β β
β (πβ(π΄βπ)) β (π΄βπ)))) |
41 | 40 | rspccv 3609 |
. . . . . . . . . . . . 13
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β ((π΄βπ) β ran π΄ β ((π΄βπ) β β
β (πβ(π΄βπ)) β (π΄βπ)))) |
42 | 35, 41 | syl5 34 |
. . . . . . . . . . . 12
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β (π β Ο β ((π΄βπ) β β
β (πβ(π΄βπ)) β (π΄βπ)))) |
43 | 32, 42 | mpdi 45 |
. . . . . . . . . . 11
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β (π β Ο β (πβ(π΄βπ)) β (π΄βπ))) |
44 | 43 | impcom 408 |
. . . . . . . . . 10
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β (πβ(π΄βπ)) β (π΄βπ)) |
45 | 9 | eleq2d 2819 |
. . . . . . . . . . 11
β’ (π β Ο β ((πβ(π΄βπ)) β (π΄βπ) β (πβ(π΄βπ)) β ({π} Γ (πΎβπ)))) |
46 | 45 | adantr 481 |
. . . . . . . . . 10
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β ((πβ(π΄βπ)) β (π΄βπ) β (πβ(π΄βπ)) β ({π} Γ (πΎβπ)))) |
47 | 44, 46 | mpbid 231 |
. . . . . . . . 9
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β (πβ(π΄βπ)) β ({π} Γ (πΎβπ))) |
48 | | xp2nd 8010 |
. . . . . . . . 9
β’ ((πβ(π΄βπ)) β ({π} Γ (πΎβπ)) β (2nd β(πβ(π΄βπ))) β (πΎβπ)) |
49 | 47, 48 | syl 17 |
. . . . . . . 8
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β (2nd β(πβ(π΄βπ))) β (πΎβπ)) |
50 | 49 | 3adant3 1132 |
. . . . . . 7
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (2nd
β(πβ(π΄βπ))) β (πΎβπ)) |
51 | 2 | fvmpt2 7009 |
. . . . . . . . . 10
β’ ((π β Ο β§
(2nd β(πβ(π΄βπ))) β V) β (πΊβπ) = (2nd β(πβ(π΄βπ)))) |
52 | 1, 51 | mpan2 689 |
. . . . . . . . 9
β’ (π β Ο β (πΊβπ) = (2nd β(πβ(π΄βπ)))) |
53 | 52 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (πΊβπ) = (2nd β(πβ(π΄βπ)))) |
54 | 53 | eqcomd 2738 |
. . . . . . 7
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (2nd
β(πβ(π΄βπ))) = (πΊβπ)) |
55 | 26 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (πΎβπ) = if((πΉβπ) = β
, {β
}, (πΉβπ))) |
56 | | ifnefalse 4540 |
. . . . . . . . 9
β’ ((πΉβπ) β β
β if((πΉβπ) = β
, {β
}, (πΉβπ)) = (πΉβπ)) |
57 | 56 | 3ad2ant3 1135 |
. . . . . . . 8
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β if((πΉβπ) = β
, {β
}, (πΉβπ)) = (πΉβπ)) |
58 | 55, 57 | eqtrd 2772 |
. . . . . . 7
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (πΎβπ) = (πΉβπ)) |
59 | 50, 54, 58 | 3eltr3d 2847 |
. . . . . 6
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§) β§ (πΉβπ) β β
) β (πΊβπ) β (πΉβπ)) |
60 | 59 | 3expia 1121 |
. . . . 5
β’ ((π β Ο β§
βπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) β ((πΉβπ) β β
β (πΊβπ) β (πΉβπ))) |
61 | 60 | expcom 414 |
. . . 4
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β (π β Ο β ((πΉβπ) β β
β (πΊβπ) β (πΉβπ)))) |
62 | 61 | ralrimiv 3145 |
. . 3
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β βπ β Ο ((πΉβπ) β β
β (πΊβπ) β (πΉβπ))) |
63 | | omex 9640 |
. . . . 5
β’ Ο
β V |
64 | | fnex 7221 |
. . . . 5
β’ ((πΊ Fn Ο β§ Ο β
V) β πΊ β
V) |
65 | 3, 63, 64 | mp2an 690 |
. . . 4
β’ πΊ β V |
66 | | fneq1 6640 |
. . . . 5
β’ (π = πΊ β (π Fn Ο β πΊ Fn Ο)) |
67 | | fveq1 6890 |
. . . . . . . 8
β’ (π = πΊ β (πβπ) = (πΊβπ)) |
68 | 67 | eleq1d 2818 |
. . . . . . 7
β’ (π = πΊ β ((πβπ) β (πΉβπ) β (πΊβπ) β (πΉβπ))) |
69 | 68 | imbi2d 340 |
. . . . . 6
β’ (π = πΊ β (((πΉβπ) β β
β (πβπ) β (πΉβπ)) β ((πΉβπ) β β
β (πΊβπ) β (πΉβπ)))) |
70 | 69 | ralbidv 3177 |
. . . . 5
β’ (π = πΊ β (βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ)) β βπ β Ο ((πΉβπ) β β
β (πΊβπ) β (πΉβπ)))) |
71 | 66, 70 | anbi12d 631 |
. . . 4
β’ (π = πΊ β ((π Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ))) β (πΊ Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πΊβπ) β (πΉβπ))))) |
72 | 65, 71 | spcev 3596 |
. . 3
β’ ((πΊ Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πΊβπ) β (πΉβπ))) β βπ(π Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ)))) |
73 | 3, 62, 72 | sylancr 587 |
. 2
β’
(βπ§ β
ran π΄(π§ β β
β (πβπ§) β π§) β βπ(π Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ)))) |
74 | 6 | a1i 11 |
. . . . . 6
β’ ((Ο
β V β§ π β
Ο) β ({π}
Γ (πΎβπ)) β V) |
75 | 74, 7 | fmptd 7115 |
. . . . 5
β’ (Ο
β V β π΄:ΟβΆV) |
76 | 63, 75 | ax-mp 5 |
. . . 4
β’ π΄:ΟβΆV |
77 | | sneq 4638 |
. . . . . . . . . 10
β’ (π = π β {π} = {π}) |
78 | | fveq2 6891 |
. . . . . . . . . 10
β’ (π = π β (πΎβπ) = (πΎβπ)) |
79 | 77, 78 | xpeq12d 5707 |
. . . . . . . . 9
β’ (π = π β ({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ))) |
80 | 79, 7, 6 | fvmpt3i 7003 |
. . . . . . . 8
β’ (π β Ο β (π΄βπ) = ({π} Γ (πΎβπ))) |
81 | 80 | adantl 482 |
. . . . . . 7
β’ ((π β Ο β§ π β Ο) β (π΄βπ) = ({π} Γ (πΎβπ))) |
82 | 81 | eqeq2d 2743 |
. . . . . 6
β’ ((π β Ο β§ π β Ο) β ((π΄βπ) = (π΄βπ) β (π΄βπ) = ({π} Γ (πΎβπ)))) |
83 | 9 | adantr 481 |
. . . . . . . 8
β’ ((π β Ο β§ π β Ο) β (π΄βπ) = ({π} Γ (πΎβπ))) |
84 | 83 | eqeq1d 2734 |
. . . . . . 7
β’ ((π β Ο β§ π β Ο) β ((π΄βπ) = ({π} Γ (πΎβπ)) β ({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)))) |
85 | | xp11 6174 |
. . . . . . . . . 10
β’ (({π} β β
β§ (πΎβπ) β β
) β (({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)) β ({π} = {π} β§ (πΎβπ) = (πΎβπ)))) |
86 | 11, 28, 85 | sylancr 587 |
. . . . . . . . 9
β’ (π β Ο β (({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)) β ({π} = {π} β§ (πΎβπ) = (πΎβπ)))) |
87 | 10 | sneqr 4841 |
. . . . . . . . . 10
β’ ({π} = {π} β π = π) |
88 | 87 | adantr 481 |
. . . . . . . . 9
β’ (({π} = {π} β§ (πΎβπ) = (πΎβπ)) β π = π) |
89 | 86, 88 | syl6bi 252 |
. . . . . . . 8
β’ (π β Ο β (({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)) β π = π)) |
90 | 89 | adantr 481 |
. . . . . . 7
β’ ((π β Ο β§ π β Ο) β (({π} Γ (πΎβπ)) = ({π} Γ (πΎβπ)) β π = π)) |
91 | 84, 90 | sylbid 239 |
. . . . . 6
β’ ((π β Ο β§ π β Ο) β ((π΄βπ) = ({π} Γ (πΎβπ)) β π = π)) |
92 | 82, 91 | sylbid 239 |
. . . . 5
β’ ((π β Ο β§ π β Ο) β ((π΄βπ) = (π΄βπ) β π = π)) |
93 | 92 | rgen2 3197 |
. . . 4
β’
βπ β
Ο βπ β
Ο ((π΄βπ) = (π΄βπ) β π = π) |
94 | | dff13 7256 |
. . . 4
β’ (π΄:Οβ1-1βV β (π΄:ΟβΆV β§ βπ β Ο βπ β Ο ((π΄βπ) = (π΄βπ) β π = π))) |
95 | 76, 93, 94 | mpbir2an 709 |
. . 3
β’ π΄:Οβ1-1βV |
96 | | f1f1orn 6844 |
. . . 4
β’ (π΄:Οβ1-1βV β π΄:Οβ1-1-ontoβran
π΄) |
97 | 63 | f1oen 8971 |
. . . 4
β’ (π΄:Οβ1-1-ontoβran
π΄ β Ο β
ran π΄) |
98 | | ensym 9001 |
. . . 4
β’ (Ο
β ran π΄ β ran
π΄ β
Ο) |
99 | 96, 97, 98 | 3syl 18 |
. . 3
β’ (π΄:Οβ1-1βV β ran π΄ β Ο) |
100 | 7 | rneqi 5936 |
. . . . 5
β’ ran π΄ = ran (π β Ο β¦ ({π} Γ (πΎβπ))) |
101 | | dmmptg 6241 |
. . . . . . . 8
β’
(βπ β
Ο ({π} Γ (πΎβπ)) β V β dom (π β Ο β¦ ({π} Γ (πΎβπ))) = Ο) |
102 | 6 | a1i 11 |
. . . . . . . 8
β’ (π β Ο β ({π} Γ (πΎβπ)) β V) |
103 | 101, 102 | mprg 3067 |
. . . . . . 7
β’ dom
(π β Ο β¦
({π} Γ (πΎβπ))) = Ο |
104 | 103, 63 | eqeltri 2829 |
. . . . . 6
β’ dom
(π β Ο β¦
({π} Γ (πΎβπ))) β V |
105 | | funmpt 6586 |
. . . . . 6
β’ Fun
(π β Ο β¦
({π} Γ (πΎβπ))) |
106 | | funrnex 7942 |
. . . . . 6
β’ (dom
(π β Ο β¦
({π} Γ (πΎβπ))) β V β (Fun (π β Ο β¦ ({π} Γ (πΎβπ))) β ran (π β Ο β¦ ({π} Γ (πΎβπ))) β V)) |
107 | 104, 105,
106 | mp2 9 |
. . . . 5
β’ ran
(π β Ο β¦
({π} Γ (πΎβπ))) β V |
108 | 100, 107 | eqeltri 2829 |
. . . 4
β’ ran π΄ β V |
109 | | breq1 5151 |
. . . . 5
β’ (π = ran π΄ β (π β Ο β ran π΄ β Ο)) |
110 | | raleq 3322 |
. . . . . 6
β’ (π = ran π΄ β (βπ§ β π (π§ β β
β (πβπ§) β π§) β βπ§ β ran π΄(π§ β β
β (πβπ§) β π§))) |
111 | 110 | exbidv 1924 |
. . . . 5
β’ (π = ran π΄ β (βπβπ§ β π (π§ β β
β (πβπ§) β π§) β βπβπ§ β ran π΄(π§ β β
β (πβπ§) β π§))) |
112 | 109, 111 | imbi12d 344 |
. . . 4
β’ (π = ran π΄ β ((π β Ο β βπβπ§ β π (π§ β β
β (πβπ§) β π§)) β (ran π΄ β Ο β βπβπ§ β ran π΄(π§ β β
β (πβπ§) β π§)))) |
113 | | ax-cc 10432 |
. . . 4
β’ (π β Ο β
βπβπ§ β π (π§ β β
β (πβπ§) β π§)) |
114 | 108, 112,
113 | vtocl 3549 |
. . 3
β’ (ran
π΄ β Ο β
βπβπ§ β ran π΄(π§ β β
β (πβπ§) β π§)) |
115 | 95, 99, 114 | mp2b 10 |
. 2
β’
βπβπ§ β ran π΄(π§ β β
β (πβπ§) β π§) |
116 | 73, 115 | exlimiiv 1934 |
1
β’
βπ(π Fn Ο β§ βπ β Ο ((πΉβπ) β β
β (πβπ) β (πΉβπ))) |