Step | Hyp | Ref
| Expression |
1 | | cc2.cc |
. . 3
β’ (π β
CCHOICE) |
2 | | vex 2738 |
. . . . . . . 8
β’ π β V |
3 | 2 | snex 4180 |
. . . . . . 7
β’ {π} β V |
4 | | cc2.a |
. . . . . . . 8
β’ (π β πΉ Fn Ο) |
5 | | funfvex 5524 |
. . . . . . . . 9
β’ ((Fun
πΉ β§ π β dom πΉ) β (πΉβπ) β V) |
6 | 5 | funfni 5308 |
. . . . . . . 8
β’ ((πΉ Fn Ο β§ π β Ο) β (πΉβπ) β V) |
7 | 4, 6 | sylan 283 |
. . . . . . 7
β’ ((π β§ π β Ο) β (πΉβπ) β V) |
8 | | xpexg 4734 |
. . . . . . 7
β’ (({π} β V β§ (πΉβπ) β V) β ({π} Γ (πΉβπ)) β V) |
9 | 3, 7, 8 | sylancr 414 |
. . . . . 6
β’ ((π β§ π β Ο) β ({π} Γ (πΉβπ)) β V) |
10 | | cc2lem.a |
. . . . . 6
β’ π΄ = (π β Ο β¦ ({π} Γ (πΉβπ))) |
11 | 9, 10 | fmptd 5662 |
. . . . 5
β’ (π β π΄:ΟβΆV) |
12 | | sneq 3600 |
. . . . . . . . . 10
β’ (π = π β {π} = {π}) |
13 | | fveq2 5507 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
14 | 12, 13 | xpeq12d 4645 |
. . . . . . . . 9
β’ (π = π β ({π} Γ (πΉβπ)) = ({π} Γ (πΉβπ))) |
15 | | simprr 531 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ π β Ο)) β π β Ο) |
16 | | vex 2738 |
. . . . . . . . . . 11
β’ π β V |
17 | 16 | snex 4180 |
. . . . . . . . . 10
β’ {π} β V |
18 | 4 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ (π β Ο β§ π β Ο)) β πΉ Fn Ο) |
19 | | funfvex 5524 |
. . . . . . . . . . . 12
β’ ((Fun
πΉ β§ π β dom πΉ) β (πΉβπ) β V) |
20 | 19 | funfni 5308 |
. . . . . . . . . . 11
β’ ((πΉ Fn Ο β§ π β Ο) β (πΉβπ) β V) |
21 | 18, 15, 20 | syl2anc 411 |
. . . . . . . . . 10
β’ ((π β§ (π β Ο β§ π β Ο)) β (πΉβπ) β V) |
22 | | xpexg 4734 |
. . . . . . . . . 10
β’ (({π} β V β§ (πΉβπ) β V) β ({π} Γ (πΉβπ)) β V) |
23 | 17, 21, 22 | sylancr 414 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ π β Ο)) β ({π} Γ (πΉβπ)) β V) |
24 | 10, 14, 15, 23 | fvmptd3 5601 |
. . . . . . . 8
β’ ((π β§ (π β Ο β§ π β Ο)) β (π΄βπ) = ({π} Γ (πΉβπ))) |
25 | 24 | eqeq2d 2187 |
. . . . . . 7
β’ ((π β§ (π β Ο β§ π β Ο)) β ((π΄βπ) = (π΄βπ) β (π΄βπ) = ({π} Γ (πΉβπ)))) |
26 | | simpr 110 |
. . . . . . . . . . 11
β’ ((π β§ π β Ο) β π β Ο) |
27 | 10 | fvmpt2 5591 |
. . . . . . . . . . 11
β’ ((π β Ο β§ ({π} Γ (πΉβπ)) β V) β (π΄βπ) = ({π} Γ (πΉβπ))) |
28 | 26, 9, 27 | syl2anc 411 |
. . . . . . . . . 10
β’ ((π β§ π β Ο) β (π΄βπ) = ({π} Γ (πΉβπ))) |
29 | 28 | adantrr 479 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ π β Ο)) β (π΄βπ) = ({π} Γ (πΉβπ))) |
30 | 29 | eqeq1d 2184 |
. . . . . . . 8
β’ ((π β§ (π β Ο β§ π β Ο)) β ((π΄βπ) = ({π} Γ (πΉβπ)) β ({π} Γ (πΉβπ)) = ({π} Γ (πΉβπ)))) |
31 | 2 | snm 3709 |
. . . . . . . . . 10
β’
βπ€ π€ β {π} |
32 | | fveq2 5507 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
33 | 32 | eleq2d 2245 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π€ β (πΉβπ₯) β π€ β (πΉβπ))) |
34 | 33 | exbidv 1823 |
. . . . . . . . . . 11
β’ (π₯ = π β (βπ€ π€ β (πΉβπ₯) β βπ€ π€ β (πΉβπ))) |
35 | | cc2.m |
. . . . . . . . . . . 12
β’ (π β βπ₯ β Ο βπ€ π€ β (πΉβπ₯)) |
36 | 35 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ (π β Ο β§ π β Ο)) β βπ₯ β Ο βπ€ π€ β (πΉβπ₯)) |
37 | | simprl 529 |
. . . . . . . . . . 11
β’ ((π β§ (π β Ο β§ π β Ο)) β π β Ο) |
38 | 34, 36, 37 | rspcdva 2844 |
. . . . . . . . . 10
β’ ((π β§ (π β Ο β§ π β Ο)) β βπ€ π€ β (πΉβπ)) |
39 | | xp11m 5059 |
. . . . . . . . . 10
β’
((βπ€ π€ β {π} β§ βπ€ π€ β (πΉβπ)) β (({π} Γ (πΉβπ)) = ({π} Γ (πΉβπ)) β ({π} = {π} β§ (πΉβπ) = (πΉβπ)))) |
40 | 31, 38, 39 | sylancr 414 |
. . . . . . . . 9
β’ ((π β§ (π β Ο β§ π β Ο)) β (({π} Γ (πΉβπ)) = ({π} Γ (πΉβπ)) β ({π} = {π} β§ (πΉβπ) = (πΉβπ)))) |
41 | 2 | sneqr 3756 |
. . . . . . . . . 10
β’ ({π} = {π} β π = π) |
42 | 41 | adantr 276 |
. . . . . . . . 9
β’ (({π} = {π} β§ (πΉβπ) = (πΉβπ)) β π = π) |
43 | 40, 42 | syl6bi 163 |
. . . . . . . 8
β’ ((π β§ (π β Ο β§ π β Ο)) β (({π} Γ (πΉβπ)) = ({π} Γ (πΉβπ)) β π = π)) |
44 | 30, 43 | sylbid 150 |
. . . . . . 7
β’ ((π β§ (π β Ο β§ π β Ο)) β ((π΄βπ) = ({π} Γ (πΉβπ)) β π = π)) |
45 | 25, 44 | sylbid 150 |
. . . . . 6
β’ ((π β§ (π β Ο β§ π β Ο)) β ((π΄βπ) = (π΄βπ) β π = π)) |
46 | 45 | ralrimivva 2557 |
. . . . 5
β’ (π β βπ β Ο βπ β Ο ((π΄βπ) = (π΄βπ) β π = π)) |
47 | | dff13 5759 |
. . . . 5
β’ (π΄:Οβ1-1βV β (π΄:ΟβΆV β§ βπ β Ο βπ β Ο ((π΄βπ) = (π΄βπ) β π = π))) |
48 | 11, 46, 47 | sylanbrc 417 |
. . . 4
β’ (π β π΄:Οβ1-1βV) |
49 | | f1f1orn 5464 |
. . . . 5
β’ (π΄:Οβ1-1βV β π΄:Οβ1-1-ontoβran
π΄) |
50 | | omex 4586 |
. . . . . 6
β’ Ο
β V |
51 | 50 | f1oen 6749 |
. . . . 5
β’ (π΄:Οβ1-1-ontoβran
π΄ β Ο β
ran π΄) |
52 | | ensym 6771 |
. . . . 5
β’ (Ο
β ran π΄ β ran
π΄ β
Ο) |
53 | 49, 51, 52 | 3syl 17 |
. . . 4
β’ (π΄:Οβ1-1βV β ran π΄ β Ο) |
54 | 48, 53 | syl 14 |
. . 3
β’ (π β ran π΄ β Ο) |
55 | 9 | ralrimiva 2548 |
. . . . . . . . 9
β’ (π β βπ β Ο ({π} Γ (πΉβπ)) β V) |
56 | 10 | fnmpt 5334 |
. . . . . . . . 9
β’
(βπ β
Ο ({π} Γ (πΉβπ)) β V β π΄ Fn Ο) |
57 | 55, 56 | syl 14 |
. . . . . . . 8
β’ (π β π΄ Fn Ο) |
58 | 57 | adantr 276 |
. . . . . . 7
β’ ((π β§ π§ β ran π΄) β π΄ Fn Ο) |
59 | | fnfun 5305 |
. . . . . . 7
β’ (π΄ Fn Ο β Fun π΄) |
60 | 58, 59 | syl 14 |
. . . . . 6
β’ ((π β§ π§ β ran π΄) β Fun π΄) |
61 | | simpr 110 |
. . . . . 6
β’ ((π β§ π§ β ran π΄) β π§ β ran π΄) |
62 | | elrnrexdm 5647 |
. . . . . 6
β’ (Fun
π΄ β (π§ β ran π΄ β βπ β dom π΄ π§ = (π΄βπ))) |
63 | 60, 61, 62 | sylc 62 |
. . . . 5
β’ ((π β§ π§ β ran π΄) β βπ β dom π΄ π§ = (π΄βπ)) |
64 | | simpll 527 |
. . . . . . 7
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β π) |
65 | | simprl 529 |
. . . . . . . 8
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β π β dom π΄) |
66 | | fndm 5307 |
. . . . . . . . 9
β’ (π΄ Fn Ο β dom π΄ = Ο) |
67 | 64, 57, 66 | 3syl 17 |
. . . . . . . 8
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β dom π΄ = Ο) |
68 | 65, 67 | eleqtrd 2254 |
. . . . . . 7
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β π β Ο) |
69 | 35 | adantr 276 |
. . . . . . . . . . 11
β’ ((π β§ π β Ο) β βπ₯ β Ο βπ€ π€ β (πΉβπ₯)) |
70 | 34, 69, 26 | rspcdva 2844 |
. . . . . . . . . 10
β’ ((π β§ π β Ο) β βπ€ π€ β (πΉβπ)) |
71 | | eleq1 2238 |
. . . . . . . . . . 11
β’ (π€ = π β (π€ β (πΉβπ) β π β (πΉβπ))) |
72 | 71 | cbvexv 1916 |
. . . . . . . . . 10
β’
(βπ€ π€ β (πΉβπ) β βπ π β (πΉβπ)) |
73 | 70, 72 | sylib 122 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β βπ π β (πΉβπ)) |
74 | | vsnid 3621 |
. . . . . . . . . . 11
β’ π β {π} |
75 | | simpr 110 |
. . . . . . . . . . 11
β’ (((π β§ π β Ο) β§ π β (πΉβπ)) β π β (πΉβπ)) |
76 | | opelxpi 4652 |
. . . . . . . . . . 11
β’ ((π β {π} β§ π β (πΉβπ)) β β¨π, πβ© β ({π} Γ (πΉβπ))) |
77 | 74, 75, 76 | sylancr 414 |
. . . . . . . . . 10
β’ (((π β§ π β Ο) β§ π β (πΉβπ)) β β¨π, πβ© β ({π} Γ (πΉβπ))) |
78 | | eleq1 2238 |
. . . . . . . . . . 11
β’ (π€ = β¨π, πβ© β (π€ β ({π} Γ (πΉβπ)) β β¨π, πβ© β ({π} Γ (πΉβπ)))) |
79 | 78 | spcegv 2823 |
. . . . . . . . . 10
β’
(β¨π, πβ© β ({π} Γ (πΉβπ)) β (β¨π, πβ© β ({π} Γ (πΉβπ)) β βπ€ π€ β ({π} Γ (πΉβπ)))) |
80 | 77, 77, 79 | sylc 62 |
. . . . . . . . 9
β’ (((π β§ π β Ο) β§ π β (πΉβπ)) β βπ€ π€ β ({π} Γ (πΉβπ))) |
81 | 73, 80 | exlimddv 1896 |
. . . . . . . 8
β’ ((π β§ π β Ο) β βπ€ π€ β ({π} Γ (πΉβπ))) |
82 | 28 | eleq2d 2245 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β (π€ β (π΄βπ) β π€ β ({π} Γ (πΉβπ)))) |
83 | 82 | exbidv 1823 |
. . . . . . . 8
β’ ((π β§ π β Ο) β (βπ€ π€ β (π΄βπ) β βπ€ π€ β ({π} Γ (πΉβπ)))) |
84 | 81, 83 | mpbird 167 |
. . . . . . 7
β’ ((π β§ π β Ο) β βπ€ π€ β (π΄βπ)) |
85 | 64, 68, 84 | syl2anc 411 |
. . . . . 6
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β βπ€ π€ β (π΄βπ)) |
86 | | simprr 531 |
. . . . . . . 8
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β π§ = (π΄βπ)) |
87 | 86 | eleq2d 2245 |
. . . . . . 7
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β (π€ β π§ β π€ β (π΄βπ))) |
88 | 87 | exbidv 1823 |
. . . . . 6
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β (βπ€ π€ β π§ β βπ€ π€ β (π΄βπ))) |
89 | 85, 88 | mpbird 167 |
. . . . 5
β’ (((π β§ π§ β ran π΄) β§ (π β dom π΄ β§ π§ = (π΄βπ))) β βπ€ π€ β π§) |
90 | 63, 89 | rexlimddv 2597 |
. . . 4
β’ ((π β§ π§ β ran π΄) β βπ€ π€ β π§) |
91 | 90 | ralrimiva 2548 |
. . 3
β’ (π β βπ§ β ran π΄βπ€ π€ β π§) |
92 | 1, 54, 91 | ccfunen 7238 |
. 2
β’ (π β βπ(π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) |
93 | | vex 2738 |
. . . . . . . 8
β’ π β V |
94 | | funfvex 5524 |
. . . . . . . . . 10
β’ ((Fun
π΄ β§ π β dom π΄) β (π΄βπ) β V) |
95 | 94 | funfni 5308 |
. . . . . . . . 9
β’ ((π΄ Fn Ο β§ π β Ο) β (π΄βπ) β V) |
96 | 57, 95 | sylan 283 |
. . . . . . . 8
β’ ((π β§ π β Ο) β (π΄βπ) β V) |
97 | | fvexg 5526 |
. . . . . . . 8
β’ ((π β V β§ (π΄βπ) β V) β (πβ(π΄βπ)) β V) |
98 | 93, 96, 97 | sylancr 414 |
. . . . . . 7
β’ ((π β§ π β Ο) β (πβ(π΄βπ)) β V) |
99 | | 2ndexg 6159 |
. . . . . . 7
β’ ((πβ(π΄βπ)) β V β (2nd
β(πβ(π΄βπ))) β V) |
100 | 98, 99 | syl 14 |
. . . . . 6
β’ ((π β§ π β Ο) β (2nd
β(πβ(π΄βπ))) β V) |
101 | 100 | ralrimiva 2548 |
. . . . 5
β’ (π β βπ β Ο (2nd β(πβ(π΄βπ))) β V) |
102 | | cc2lem.g |
. . . . . 6
β’ πΊ = (π β Ο β¦ (2nd
β(πβ(π΄βπ)))) |
103 | 102 | fnmpt 5334 |
. . . . 5
β’
(βπ β
Ο (2nd β(πβ(π΄βπ))) β V β πΊ Fn Ο) |
104 | 101, 103 | syl 14 |
. . . 4
β’ (π β πΊ Fn Ο) |
105 | 104 | adantr 276 |
. . 3
β’ ((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β πΊ Fn Ο) |
106 | | simpr 110 |
. . . . . 6
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β π β Ο) |
107 | | fveq2 5507 |
. . . . . . . . . 10
β’ (π§ = (π΄βπ) β (πβπ§) = (πβ(π΄βπ))) |
108 | | id 19 |
. . . . . . . . . 10
β’ (π§ = (π΄βπ) β π§ = (π΄βπ)) |
109 | 107, 108 | eleq12d 2246 |
. . . . . . . . 9
β’ (π§ = (π΄βπ) β ((πβπ§) β π§ β (πβ(π΄βπ)) β (π΄βπ))) |
110 | | simplrr 536 |
. . . . . . . . 9
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β βπ§ β ran π΄(πβπ§) β π§) |
111 | | fnfvelrn 5640 |
. . . . . . . . . . 11
β’ ((π΄ Fn Ο β§ π β Ο) β (π΄βπ) β ran π΄) |
112 | 57, 111 | sylan 283 |
. . . . . . . . . 10
β’ ((π β§ π β Ο) β (π΄βπ) β ran π΄) |
113 | 112 | adantlr 477 |
. . . . . . . . 9
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β (π΄βπ) β ran π΄) |
114 | 109, 110,
113 | rspcdva 2844 |
. . . . . . . 8
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β (πβ(π΄βπ)) β (π΄βπ)) |
115 | 28 | eleq2d 2245 |
. . . . . . . . 9
β’ ((π β§ π β Ο) β ((πβ(π΄βπ)) β (π΄βπ) β (πβ(π΄βπ)) β ({π} Γ (πΉβπ)))) |
116 | 115 | adantlr 477 |
. . . . . . . 8
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β ((πβ(π΄βπ)) β (π΄βπ) β (πβ(π΄βπ)) β ({π} Γ (πΉβπ)))) |
117 | 114, 116 | mpbid 147 |
. . . . . . 7
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β (πβ(π΄βπ)) β ({π} Γ (πΉβπ))) |
118 | | xp2nd 6157 |
. . . . . . 7
β’ ((πβ(π΄βπ)) β ({π} Γ (πΉβπ)) β (2nd β(πβ(π΄βπ))) β (πΉβπ)) |
119 | 117, 118 | syl 14 |
. . . . . 6
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β (2nd
β(πβ(π΄βπ))) β (πΉβπ)) |
120 | 102 | fvmpt2 5591 |
. . . . . 6
β’ ((π β Ο β§
(2nd β(πβ(π΄βπ))) β (πΉβπ)) β (πΊβπ) = (2nd β(πβ(π΄βπ)))) |
121 | 106, 119,
120 | syl2anc 411 |
. . . . 5
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β (πΊβπ) = (2nd β(πβ(π΄βπ)))) |
122 | 121, 119 | eqeltrd 2252 |
. . . 4
β’ (((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β§ π β Ο) β (πΊβπ) β (πΉβπ)) |
123 | 122 | ralrimiva 2548 |
. . 3
β’ ((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β βπ β Ο (πΊβπ) β (πΉβπ)) |
124 | 50 | a1i 9 |
. . . . . 6
β’ (π β Ο β
V) |
125 | | fnex 5730 |
. . . . . 6
β’ ((πΊ Fn Ο β§ Ο β
V) β πΊ β
V) |
126 | 104, 124,
125 | syl2anc 411 |
. . . . 5
β’ (π β πΊ β V) |
127 | | fneq1 5296 |
. . . . . . 7
β’ (π = πΊ β (π Fn Ο β πΊ Fn Ο)) |
128 | | fveq1 5506 |
. . . . . . . . 9
β’ (π = πΊ β (πβπ) = (πΊβπ)) |
129 | 128 | eleq1d 2244 |
. . . . . . . 8
β’ (π = πΊ β ((πβπ) β (πΉβπ) β (πΊβπ) β (πΉβπ))) |
130 | 129 | ralbidv 2475 |
. . . . . . 7
β’ (π = πΊ β (βπ β Ο (πβπ) β (πΉβπ) β βπ β Ο (πΊβπ) β (πΉβπ))) |
131 | 127, 130 | anbi12d 473 |
. . . . . 6
β’ (π = πΊ β ((π Fn Ο β§ βπ β Ο (πβπ) β (πΉβπ)) β (πΊ Fn Ο β§ βπ β Ο (πΊβπ) β (πΉβπ)))) |
132 | 131 | spcegv 2823 |
. . . . 5
β’ (πΊ β V β ((πΊ Fn Ο β§ βπ β Ο (πΊβπ) β (πΉβπ)) β βπ(π Fn Ο β§ βπ β Ο (πβπ) β (πΉβπ)))) |
133 | 126, 132 | syl 14 |
. . . 4
β’ (π β ((πΊ Fn Ο β§ βπ β Ο (πΊβπ) β (πΉβπ)) β βπ(π Fn Ο β§ βπ β Ο (πβπ) β (πΉβπ)))) |
134 | 133 | adantr 276 |
. . 3
β’ ((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β ((πΊ Fn Ο β§ βπ β Ο (πΊβπ) β (πΉβπ)) β βπ(π Fn Ο β§ βπ β Ο (πβπ) β (πΉβπ)))) |
135 | 105, 123,
134 | mp2and 433 |
. 2
β’ ((π β§ (π Fn ran π΄ β§ βπ§ β ran π΄(πβπ§) β π§)) β βπ(π Fn Ο β§ βπ β Ο (πβπ) β (πΉβπ))) |
136 | 92, 135 | exlimddv 1896 |
1
β’ (π β βπ(π Fn Ο β§ βπ β Ο (πβπ) β (πΉβπ))) |