Step | Hyp | Ref
| Expression |
1 | | n0 4307 |
. . . 4
β’ (π β β
β
βπ₯ π₯ β π) |
2 | | 0ss 4357 |
. . . . . . . . . 10
β’ β
β π₯ |
3 | | gruss 10737 |
. . . . . . . . . 10
β’ ((π β Univ β§ π₯ β π β§ β
β π₯) β β
β π) |
4 | 2, 3 | mp3an3 1451 |
. . . . . . . . 9
β’ ((π β Univ β§ π₯ β π) β β
β π) |
5 | | 0elon 6372 |
. . . . . . . . 9
β’ β
β On |
6 | | elin 3927 |
. . . . . . . . 9
β’ (β
β (π β© On) β
(β
β π β§
β
β On)) |
7 | 4, 5, 6 | sylanblrc 591 |
. . . . . . . 8
β’ ((π β Univ β§ π₯ β π) β β
β (π β© On)) |
8 | | gruina.1 |
. . . . . . . 8
β’ π΄ = (π β© On) |
9 | 7, 8 | eleqtrrdi 2845 |
. . . . . . 7
β’ ((π β Univ β§ π₯ β π) β β
β π΄) |
10 | 9 | ne0d 4296 |
. . . . . 6
β’ ((π β Univ β§ π₯ β π) β π΄ β β
) |
11 | 10 | expcom 415 |
. . . . 5
β’ (π₯ β π β (π β Univ β π΄ β β
)) |
12 | 11 | exlimiv 1934 |
. . . 4
β’
(βπ₯ π₯ β π β (π β Univ β π΄ β β
)) |
13 | 1, 12 | sylbi 216 |
. . 3
β’ (π β β
β (π β Univ β π΄ β β
)) |
14 | 13 | impcom 409 |
. 2
β’ ((π β Univ β§ π β β
) β π΄ β β
) |
15 | | grutr 10734 |
. . . . . . . 8
β’ (π β Univ β Tr π) |
16 | | tron 6341 |
. . . . . . . 8
β’ Tr
On |
17 | | trin 5235 |
. . . . . . . 8
β’ ((Tr
π β§ Tr On) β Tr
(π β©
On)) |
18 | 15, 16, 17 | sylancl 587 |
. . . . . . 7
β’ (π β Univ β Tr (π β© On)) |
19 | | inss2 4190 |
. . . . . . . 8
β’ (π β© On) β
On |
20 | | epweon 7710 |
. . . . . . . 8
β’ E We
On |
21 | | wess 5621 |
. . . . . . . 8
β’ ((π β© On) β On β ( E
We On β E We (π β©
On))) |
22 | 19, 20, 21 | mp2 9 |
. . . . . . 7
β’ E We
(π β©
On) |
23 | | df-ord 6321 |
. . . . . . 7
β’ (Ord
(π β© On) β (Tr
(π β© On) β§ E We
(π β©
On))) |
24 | 18, 22, 23 | sylanblrc 591 |
. . . . . 6
β’ (π β Univ β Ord (π β© On)) |
25 | | inex1g 5277 |
. . . . . 6
β’ (π β Univ β (π β© On) β
V) |
26 | | elon2 6329 |
. . . . . 6
β’ ((π β© On) β On β (Ord
(π β© On) β§ (π β© On) β
V)) |
27 | 24, 25, 26 | sylanbrc 584 |
. . . . 5
β’ (π β Univ β (π β© On) β
On) |
28 | 8, 27 | eqeltrid 2838 |
. . . 4
β’ (π β Univ β π΄ β On) |
29 | 28 | adantr 482 |
. . 3
β’ ((π β Univ β§ π β β
) β π΄ β On) |
30 | | eloni 6328 |
. . . . . . 7
β’ (π΄ β On β Ord π΄) |
31 | | ordirr 6336 |
. . . . . . 7
β’ (Ord
π΄ β Β¬ π΄ β π΄) |
32 | 30, 31 | syl 17 |
. . . . . 6
β’ (π΄ β On β Β¬ π΄ β π΄) |
33 | | elin 3927 |
. . . . . . . . 9
β’ (π΄ β (π β© On) β (π΄ β π β§ π΄ β On)) |
34 | 33 | biimpri 227 |
. . . . . . . 8
β’ ((π΄ β π β§ π΄ β On) β π΄ β (π β© On)) |
35 | 34, 8 | eleqtrrdi 2845 |
. . . . . . 7
β’ ((π΄ β π β§ π΄ β On) β π΄ β π΄) |
36 | 35 | expcom 415 |
. . . . . 6
β’ (π΄ β On β (π΄ β π β π΄ β π΄)) |
37 | 32, 36 | mtod 197 |
. . . . 5
β’ (π΄ β On β Β¬ π΄ β π) |
38 | 29, 37 | syl 17 |
. . . 4
β’ ((π β Univ β§ π β β
) β Β¬
π΄ β π) |
39 | | inss1 4189 |
. . . . . . . . . . . . . . . 16
β’ (π β© On) β π |
40 | 8, 39 | eqsstri 3979 |
. . . . . . . . . . . . . . 15
β’ π΄ β π |
41 | 40 | sseli 3941 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β π₯ β π) |
42 | | vpwex 5333 |
. . . . . . . . . . . . . . . 16
β’ π«
π₯ β V |
43 | 42 | canth2 9077 |
. . . . . . . . . . . . . . 15
β’ π«
π₯ βΊ π«
π« π₯ |
44 | 42 | pwex 5336 |
. . . . . . . . . . . . . . . . . 18
β’ π«
π« π₯ β
V |
45 | 44 | cardid 10488 |
. . . . . . . . . . . . . . . . 17
β’
(cardβπ« π« π₯) β π« π« π₯ |
46 | 45 | ensymi 8947 |
. . . . . . . . . . . . . . . 16
β’ π«
π« π₯ β
(cardβπ« π« π₯) |
47 | 28 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Univ β§ π₯ β π) β π΄ β On) |
48 | | grupw 10736 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Univ β§ π₯ β π) β π« π₯ β π) |
49 | | grupw 10736 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Univ β§ π«
π₯ β π) β π« π« π₯ β π) |
50 | 48, 49 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Univ β§ π₯ β π) β π« π« π₯ β π) |
51 | 28 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Univ β§ π«
π« π₯ β π) β π΄ β On) |
52 | | endom 8922 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((cardβπ« π« π₯) β π« π« π₯ β (cardβπ«
π« π₯) βΌ
π« π« π₯) |
53 | 45, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(cardβπ« π« π₯) βΌ π« π« π₯ |
54 | | cardon 9885 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(cardβπ« π« π₯) β On |
55 | | grudomon 10758 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Univ β§
(cardβπ« π« π₯) β On β§ (π« π« π₯ β π β§ (cardβπ« π« π₯) βΌ π« π«
π₯)) β
(cardβπ« π« π₯) β π) |
56 | 54, 55 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Univ β§ (π«
π« π₯ β π β§ (cardβπ«
π« π₯) βΌ
π« π« π₯))
β (cardβπ« π« π₯) β π) |
57 | 53, 56 | mpanr2 703 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Univ β§ π«
π« π₯ β π) β (cardβπ«
π« π₯) β π) |
58 | | elin 3927 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((cardβπ« π« π₯) β (π β© On) β ((cardβπ«
π« π₯) β π β§ (cardβπ«
π« π₯) β
On)) |
59 | 58 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((cardβπ« π« π₯) β π β§ (cardβπ« π« π₯) β On) β
(cardβπ« π« π₯) β (π β© On)) |
60 | 59, 8 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((cardβπ« π« π₯) β π β§ (cardβπ« π« π₯) β On) β
(cardβπ« π« π₯) β π΄) |
61 | 57, 54, 60 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Univ β§ π«
π« π₯ β π) β (cardβπ«
π« π₯) β π΄) |
62 | | onelss 6360 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β On β
((cardβπ« π« π₯) β π΄ β (cardβπ« π«
π₯) β π΄)) |
63 | 51, 61, 62 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Univ β§ π«
π« π₯ β π) β (cardβπ«
π« π₯) β π΄) |
64 | 50, 63 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Univ β§ π₯ β π) β (cardβπ« π«
π₯) β π΄) |
65 | | ssdomg 8943 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β On β
((cardβπ« π« π₯) β π΄ β (cardβπ« π«
π₯) βΌ π΄)) |
66 | 47, 64, 65 | sylc 65 |
. . . . . . . . . . . . . . . 16
β’ ((π β Univ β§ π₯ β π) β (cardβπ« π«
π₯) βΌ π΄) |
67 | | endomtr 8955 |
. . . . . . . . . . . . . . . 16
β’
((π« π« π₯ β (cardβπ« π«
π₯) β§
(cardβπ« π« π₯) βΌ π΄) β π« π« π₯ βΌ π΄) |
68 | 46, 66, 67 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ ((π β Univ β§ π₯ β π) β π« π« π₯ βΌ π΄) |
69 | | sdomdomtr 9057 |
. . . . . . . . . . . . . . 15
β’
((π« π₯
βΊ π« π« π₯ β§ π« π« π₯ βΌ π΄) β π« π₯ βΊ π΄) |
70 | 43, 68, 69 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ ((π β Univ β§ π₯ β π) β π« π₯ βΊ π΄) |
71 | 41, 70 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β Univ β§ π₯ β π΄) β π« π₯ βΊ π΄) |
72 | 71 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (π β Univ β
βπ₯ β π΄ π« π₯ βΊ π΄) |
73 | | inawinalem 10630 |
. . . . . . . . . . . 12
β’ (π΄ β On β (βπ₯ β π΄ π« π₯ βΊ π΄ β βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦)) |
74 | 28, 72, 73 | sylc 65 |
. . . . . . . . . . 11
β’ (π β Univ β
βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦) |
75 | 74 | adantr 482 |
. . . . . . . . . 10
β’ ((π β Univ β§ π β β
) β
βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦) |
76 | | winainflem 10634 |
. . . . . . . . . 10
β’ ((π΄ β β
β§ π΄ β On β§ βπ₯ β π΄ βπ¦ β π΄ π₯ βΊ π¦) β Ο β π΄) |
77 | 14, 29, 75, 76 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β Univ β§ π β β
) β Ο
β π΄) |
78 | | vex 3448 |
. . . . . . . . . . . . . . 15
β’ π₯ β V |
79 | 78 | canth2 9077 |
. . . . . . . . . . . . . 14
β’ π₯ βΊ π« π₯ |
80 | | sdomtr 9062 |
. . . . . . . . . . . . . 14
β’ ((π₯ βΊ π« π₯ β§ π« π₯ βΊ π΄) β π₯ βΊ π΄) |
81 | 79, 71, 80 | sylancr 588 |
. . . . . . . . . . . . 13
β’ ((π β Univ β§ π₯ β π΄) β π₯ βΊ π΄) |
82 | 81 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ (π β Univ β
βπ₯ β π΄ π₯ βΊ π΄) |
83 | | iscard 9916 |
. . . . . . . . . . . 12
β’
((cardβπ΄) =
π΄ β (π΄ β On β§ βπ₯ β π΄ π₯ βΊ π΄)) |
84 | 28, 82, 83 | sylanbrc 584 |
. . . . . . . . . . 11
β’ (π β Univ β
(cardβπ΄) = π΄) |
85 | | cardlim 9913 |
. . . . . . . . . . . 12
β’ (Ο
β (cardβπ΄)
β Lim (cardβπ΄)) |
86 | | sseq2 3971 |
. . . . . . . . . . . . 13
β’
((cardβπ΄) =
π΄ β (Ο β
(cardβπ΄) β
Ο β π΄)) |
87 | | limeq 6330 |
. . . . . . . . . . . . 13
β’
((cardβπ΄) =
π΄ β (Lim
(cardβπ΄) β Lim
π΄)) |
88 | 86, 87 | bibi12d 346 |
. . . . . . . . . . . 12
β’
((cardβπ΄) =
π΄ β ((Ο β
(cardβπ΄) β Lim
(cardβπ΄)) β
(Ο β π΄ β
Lim π΄))) |
89 | 85, 88 | mpbii 232 |
. . . . . . . . . . 11
β’
((cardβπ΄) =
π΄ β (Ο β
π΄ β Lim π΄)) |
90 | 84, 89 | syl 17 |
. . . . . . . . . 10
β’ (π β Univ β (Ο
β π΄ β Lim π΄)) |
91 | 90 | adantr 482 |
. . . . . . . . 9
β’ ((π β Univ β§ π β β
) β (Ο
β π΄ β Lim π΄)) |
92 | 77, 91 | mpbid 231 |
. . . . . . . 8
β’ ((π β Univ β§ π β β
) β Lim π΄) |
93 | | cflm 10191 |
. . . . . . . 8
β’ ((π΄ β On β§ Lim π΄) β (cfβπ΄) = β©
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))}) |
94 | 29, 92, 93 | syl2anc 585 |
. . . . . . 7
β’ ((π β Univ β§ π β β
) β
(cfβπ΄) = β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))}) |
95 | | cardon 9885 |
. . . . . . . . . . . 12
β’
(cardβπ¦)
β On |
96 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π₯ = (cardβπ¦) β (π₯ β On β (cardβπ¦) β On)) |
97 | 95, 96 | mpbiri 258 |
. . . . . . . . . . 11
β’ (π₯ = (cardβπ¦) β π₯ β On) |
98 | 97 | adantr 482 |
. . . . . . . . . 10
β’ ((π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β π₯ β On) |
99 | 98 | exlimiv 1934 |
. . . . . . . . 9
β’
(βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β π₯ β On) |
100 | 99 | abssi 4028 |
. . . . . . . 8
β’ {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β On |
101 | | fvex 6856 |
. . . . . . . . . 10
β’
(cfβπ΄) β
V |
102 | 94, 101 | eqeltrrdi 2843 |
. . . . . . . . 9
β’ ((π β Univ β§ π β β
) β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β V) |
103 | | intex 5295 |
. . . . . . . . 9
β’ ({π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β β
β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β V) |
104 | 102, 103 | sylibr 233 |
. . . . . . . 8
β’ ((π β Univ β§ π β β
) β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β
β
) |
105 | | onint 7726 |
. . . . . . . 8
β’ (({π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β On β§ {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β β
) β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))}) |
106 | 100, 104,
105 | sylancr 588 |
. . . . . . 7
β’ ((π β Univ β§ π β β
) β β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))}) |
107 | 94, 106 | eqeltrd 2834 |
. . . . . 6
β’ ((π β Univ β§ π β β
) β
(cfβπ΄) β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))}) |
108 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π₯ = (cfβπ΄) β (π₯ = (cardβπ¦) β (cfβπ΄) = (cardβπ¦))) |
109 | 108 | anbi1d 631 |
. . . . . . . 8
β’ (π₯ = (cfβπ΄) β ((π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β ((cfβπ΄) = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)))) |
110 | 109 | exbidv 1925 |
. . . . . . 7
β’ (π₯ = (cfβπ΄) β (βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β βπ¦((cfβπ΄) = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)))) |
111 | 101, 110 | elab 3631 |
. . . . . 6
β’
((cfβπ΄) β
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))} β βπ¦((cfβπ΄) = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))) |
112 | 107, 111 | sylib 217 |
. . . . 5
β’ ((π β Univ β§ π β β
) β
βπ¦((cfβπ΄) = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦))) |
113 | | simp2rr 1244 |
. . . . . . . 8
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β π΄ = βͺ π¦) |
114 | | simp1l 1198 |
. . . . . . . . 9
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β π β Univ) |
115 | | simp2rl 1243 |
. . . . . . . . . . 11
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β π¦ β π΄) |
116 | 115, 40 | sstrdi 3957 |
. . . . . . . . . 10
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β π¦ β π) |
117 | 40 | sseli 3941 |
. . . . . . . . . . 11
β’
((cfβπ΄) β
π΄ β (cfβπ΄) β π) |
118 | 117 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β (cfβπ΄) β π) |
119 | | simp2l 1200 |
. . . . . . . . . . 11
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β (cfβπ΄) = (cardβπ¦)) |
120 | | vex 3448 |
. . . . . . . . . . . 12
β’ π¦ β V |
121 | 120 | cardid 10488 |
. . . . . . . . . . 11
β’
(cardβπ¦)
β π¦ |
122 | 119, 121 | eqbrtrdi 5145 |
. . . . . . . . . 10
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β (cfβπ΄) β π¦) |
123 | | gruen 10753 |
. . . . . . . . . 10
β’ ((π β Univ β§ π¦ β π β§ ((cfβπ΄) β π β§ (cfβπ΄) β π¦)) β π¦ β π) |
124 | 114, 116,
118, 122, 123 | syl112anc 1375 |
. . . . . . . . 9
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β π¦ β π) |
125 | | gruuni 10741 |
. . . . . . . . 9
β’ ((π β Univ β§ π¦ β π) β βͺ π¦ β π) |
126 | 114, 124,
125 | syl2anc 585 |
. . . . . . . 8
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β βͺ π¦ β π) |
127 | 113, 126 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β Univ β§ π β β
) β§
((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β§ (cfβπ΄) β π΄) β π΄ β π) |
128 | 127 | 3exp 1120 |
. . . . . 6
β’ ((π β Univ β§ π β β
) β
(((cfβπ΄) =
(cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β ((cfβπ΄) β π΄ β π΄ β π))) |
129 | 128 | exlimdv 1937 |
. . . . 5
β’ ((π β Univ β§ π β β
) β
(βπ¦((cfβπ΄) = (cardβπ¦) β§ (π¦ β π΄ β§ π΄ = βͺ π¦)) β ((cfβπ΄) β π΄ β π΄ β π))) |
130 | 112, 129 | mpd 15 |
. . . 4
β’ ((π β Univ β§ π β β
) β
((cfβπ΄) β π΄ β π΄ β π)) |
131 | 38, 130 | mtod 197 |
. . 3
β’ ((π β Univ β§ π β β
) β Β¬
(cfβπ΄) β π΄) |
132 | | cfon 10196 |
. . . . 5
β’
(cfβπ΄) β
On |
133 | | cfle 10195 |
. . . . . 6
β’
(cfβπ΄) β
π΄ |
134 | | onsseleq 6359 |
. . . . . 6
β’
(((cfβπ΄)
β On β§ π΄ β
On) β ((cfβπ΄)
β π΄ β
((cfβπ΄) β π΄ β¨ (cfβπ΄) = π΄))) |
135 | 133, 134 | mpbii 232 |
. . . . 5
β’
(((cfβπ΄)
β On β§ π΄ β
On) β ((cfβπ΄)
β π΄ β¨
(cfβπ΄) = π΄)) |
136 | 132, 135 | mpan 689 |
. . . 4
β’ (π΄ β On β
((cfβπ΄) β π΄ β¨ (cfβπ΄) = π΄)) |
137 | 136 | ord 863 |
. . 3
β’ (π΄ β On β (Β¬
(cfβπ΄) β π΄ β (cfβπ΄) = π΄)) |
138 | 29, 131, 137 | sylc 65 |
. 2
β’ ((π β Univ β§ π β β
) β
(cfβπ΄) = π΄) |
139 | 72 | adantr 482 |
. 2
β’ ((π β Univ β§ π β β
) β
βπ₯ β π΄ π« π₯ βΊ π΄) |
140 | | elina 10628 |
. 2
β’ (π΄ β Inacc β (π΄ β β
β§
(cfβπ΄) = π΄ β§ βπ₯ β π΄ π« π₯ βΊ π΄)) |
141 | 14, 138, 139, 140 | syl3anbrc 1344 |
1
β’ ((π β Univ β§ π β β
) β π΄ β Inacc) |