Step | Hyp | Ref
| Expression |
1 | | cardeq0 10546 |
. . . 4
β’ (π β Tarski β
((cardβπ) = β
β π =
β
)) |
2 | 1 | necon3bid 2979 |
. . 3
β’ (π β Tarski β
((cardβπ) β
β
β π β
β
)) |
3 | 2 | biimpar 477 |
. 2
β’ ((π β Tarski β§ π β β
) β
(cardβπ) β
β
) |
4 | | eqid 2726 |
. . . . . 6
β’ (π§ β
(cfβ(β΅ββ© {π₯ β On β£ (cardβπ) β (β΅βπ₯)})) β¦ (harβ(π€βπ§))) = (π§ β (cfβ(β΅ββ© {π₯
β On β£ (cardβπ) β (β΅βπ₯)})) β¦ (harβ(π€βπ§))) |
5 | 4 | pwcfsdom 10577 |
. . . . 5
β’
(β΅ββ© {π₯ β On β£ (cardβπ) β (β΅βπ₯)}) βΊ
((β΅ββ© {π₯ β On β£ (cardβπ) β (β΅βπ₯)}) βm
(cfβ(β΅ββ© {π₯ β On β£ (cardβπ) β (β΅βπ₯)}))) |
6 | | vpwex 5368 |
. . . . . . . . . . . 12
β’ π«
π₯ β V |
7 | 6 | canth2 9129 |
. . . . . . . . . . 11
β’ π«
π₯ βΊ π«
π« π₯ |
8 | | simpl 482 |
. . . . . . . . . . . . 13
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π β Tarski) |
9 | | cardon 9938 |
. . . . . . . . . . . . . . . . 17
β’
(cardβπ)
β On |
10 | 9 | oneli 6471 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (cardβπ) β π₯ β On) |
11 | 10 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π₯ β On) |
12 | | cardsdomelir 9967 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (cardβπ) β π₯ βΊ π) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . . 15
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π₯ βΊ π) |
14 | | tskord 10774 |
. . . . . . . . . . . . . . 15
β’ ((π β Tarski β§ π₯ β On β§ π₯ βΊ π) β π₯ β π) |
15 | 8, 11, 13, 14 | syl3anc 1368 |
. . . . . . . . . . . . . 14
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π₯ β π) |
16 | | tskpw 10747 |
. . . . . . . . . . . . . . 15
β’ ((π β Tarski β§ π₯ β π) β π« π₯ β π) |
17 | | tskpwss 10746 |
. . . . . . . . . . . . . . 15
β’ ((π β Tarski β§ π«
π₯ β π) β π« π« π₯ β π) |
18 | 16, 17 | syldan 590 |
. . . . . . . . . . . . . 14
β’ ((π β Tarski β§ π₯ β π) β π« π« π₯ β π) |
19 | 15, 18 | syldan 590 |
. . . . . . . . . . . . 13
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π« π«
π₯ β π) |
20 | | ssdomg 8995 |
. . . . . . . . . . . . 13
β’ (π β Tarski β (π«
π« π₯ β π β π« π«
π₯ βΌ π)) |
21 | 8, 19, 20 | sylc 65 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π« π«
π₯ βΌ π) |
22 | | cardidg 10542 |
. . . . . . . . . . . . . 14
β’ (π β Tarski β
(cardβπ) β
π) |
23 | 22 | ensymd 9000 |
. . . . . . . . . . . . 13
β’ (π β Tarski β π β (cardβπ)) |
24 | 23 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π β (cardβπ)) |
25 | | domentr 9008 |
. . . . . . . . . . . 12
β’
((π« π« π₯ βΌ π β§ π β (cardβπ)) β π« π« π₯ βΌ (cardβπ)) |
26 | 21, 24, 25 | syl2anc 583 |
. . . . . . . . . . 11
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π« π«
π₯ βΌ (cardβπ)) |
27 | | sdomdomtr 9109 |
. . . . . . . . . . 11
β’
((π« π₯
βΊ π« π« π₯ β§ π« π« π₯ βΌ (cardβπ)) β π« π₯ βΊ (cardβπ)) |
28 | 7, 26, 27 | sylancr 586 |
. . . . . . . . . 10
β’ ((π β Tarski β§ π₯ β (cardβπ)) β π« π₯ βΊ (cardβπ)) |
29 | 28 | ralrimiva 3140 |
. . . . . . . . 9
β’ (π β Tarski β
βπ₯ β
(cardβπ)π«
π₯ βΊ (cardβπ)) |
30 | 29 | adantr 480 |
. . . . . . . 8
β’ ((π β Tarski β§ π β β
) β
βπ₯ β
(cardβπ)π«
π₯ βΊ (cardβπ)) |
31 | | inawinalem 10683 |
. . . . . . . . . 10
β’
((cardβπ)
β On β (βπ₯
β (cardβπ)π« π₯ βΊ (cardβπ) β βπ₯ β (cardβπ)βπ¦ β (cardβπ)π₯ βΊ π¦)) |
32 | 9, 31 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ₯ β
(cardβπ)π«
π₯ βΊ (cardβπ) β βπ₯ β (cardβπ)βπ¦ β (cardβπ)π₯ βΊ π¦) |
33 | | winainflem 10687 |
. . . . . . . . . 10
β’
(((cardβπ)
β β
β§ (cardβπ) β On β§ βπ₯ β (cardβπ)βπ¦ β (cardβπ)π₯ βΊ π¦) β Ο β (cardβπ)) |
34 | 9, 33 | mp3an2 1445 |
. . . . . . . . 9
β’
(((cardβπ)
β β
β§ βπ₯ β (cardβπ)βπ¦ β (cardβπ)π₯ βΊ π¦) β Ο β (cardβπ)) |
35 | 32, 34 | sylan2 592 |
. . . . . . . 8
β’
(((cardβπ)
β β
β§ βπ₯ β (cardβπ)π« π₯ βΊ (cardβπ)) β Ο β (cardβπ)) |
36 | 3, 30, 35 | syl2anc 583 |
. . . . . . 7
β’ ((π β Tarski β§ π β β
) β Ο
β (cardβπ)) |
37 | | cardidm 9953 |
. . . . . . 7
β’
(cardβ(cardβπ)) = (cardβπ) |
38 | | cardaleph 10083 |
. . . . . . 7
β’ ((Ο
β (cardβπ)
β§ (cardβ(cardβπ)) = (cardβπ)) β (cardβπ) = (β΅ββ© {π₯
β On β£ (cardβπ) β (β΅βπ₯)})) |
39 | 36, 37, 38 | sylancl 585 |
. . . . . 6
β’ ((π β Tarski β§ π β β
) β
(cardβπ) =
(β΅ββ© {π₯ β On β£ (cardβπ) β (β΅βπ₯)})) |
40 | 39 | fveq2d 6888 |
. . . . . . 7
β’ ((π β Tarski β§ π β β
) β
(cfβ(cardβπ)) =
(cfβ(β΅ββ© {π₯ β On β£ (cardβπ) β (β΅βπ₯)}))) |
41 | 39, 40 | oveq12d 7422 |
. . . . . 6
β’ ((π β Tarski β§ π β β
) β
((cardβπ)
βm (cfβ(cardβπ))) = ((β΅ββ© {π₯
β On β£ (cardβπ) β (β΅βπ₯)}) βm
(cfβ(β΅ββ© {π₯ β On β£ (cardβπ) β (β΅βπ₯)})))) |
42 | 39, 41 | breq12d 5154 |
. . . . 5
β’ ((π β Tarski β§ π β β
) β
((cardβπ) βΊ
((cardβπ)
βm (cfβ(cardβπ))) β (β΅ββ© {π₯
β On β£ (cardβπ) β (β΅βπ₯)}) βΊ ((β΅ββ© {π₯
β On β£ (cardβπ) β (β΅βπ₯)}) βm
(cfβ(β΅ββ© {π₯ β On β£ (cardβπ) β (β΅βπ₯)}))))) |
43 | 5, 42 | mpbiri 258 |
. . . 4
β’ ((π β Tarski β§ π β β
) β
(cardβπ) βΊ
((cardβπ)
βm (cfβ(cardβπ)))) |
44 | | simp1 1133 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ) β§
π₯ β ((cardβπ) βm
(cfβ(cardβπ))))
β π β
Tarski) |
45 | | simp3 1135 |
. . . . . . . . . . . . 13
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ) β§
π₯ β ((cardβπ) βm
(cfβ(cardβπ))))
β π₯ β
((cardβπ)
βm (cfβ(cardβπ)))) |
46 | | fvex 6897 |
. . . . . . . . . . . . . . . 16
β’
(cardβπ)
β V |
47 | | fvex 6897 |
. . . . . . . . . . . . . . . 16
β’
(cfβ(cardβπ)) β V |
48 | 46, 47 | elmap 8864 |
. . . . . . . . . . . . . . 15
β’ (π₯ β ((cardβπ) βm
(cfβ(cardβπ)))
β π₯:(cfβ(cardβπ))βΆ(cardβπ)) |
49 | | fssxp 6738 |
. . . . . . . . . . . . . . 15
β’ (π₯:(cfβ(cardβπ))βΆ(cardβπ) β π₯ β ((cfβ(cardβπ)) Γ (cardβπ))) |
50 | 48, 49 | sylbi 216 |
. . . . . . . . . . . . . 14
β’ (π₯ β ((cardβπ) βm
(cfβ(cardβπ)))
β π₯ β
((cfβ(cardβπ))
Γ (cardβπ))) |
51 | 15 | ex 412 |
. . . . . . . . . . . . . . . 16
β’ (π β Tarski β (π₯ β (cardβπ) β π₯ β π)) |
52 | 51 | ssrdv 3983 |
. . . . . . . . . . . . . . 15
β’ (π β Tarski β
(cardβπ) β
π) |
53 | | cfle 10248 |
. . . . . . . . . . . . . . . . 17
β’
(cfβ(cardβπ)) β (cardβπ) |
54 | | sstr 3985 |
. . . . . . . . . . . . . . . . 17
β’
(((cfβ(cardβπ)) β (cardβπ) β§ (cardβπ) β π) β (cfβ(cardβπ)) β π) |
55 | 53, 54 | mpan 687 |
. . . . . . . . . . . . . . . 16
β’
((cardβπ)
β π β
(cfβ(cardβπ))
β π) |
56 | | tskxpss 10766 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Tarski β§
(cfβ(cardβπ))
β π β§
(cardβπ) β
π) β
((cfβ(cardβπ))
Γ (cardβπ))
β π) |
57 | 56 | 3exp 1116 |
. . . . . . . . . . . . . . . . 17
β’ (π β Tarski β
((cfβ(cardβπ))
β π β
((cardβπ) β
π β
((cfβ(cardβπ))
Γ (cardβπ))
β π))) |
58 | 57 | com23 86 |
. . . . . . . . . . . . . . . 16
β’ (π β Tarski β
((cardβπ) β
π β
((cfβ(cardβπ))
β π β
((cfβ(cardβπ))
Γ (cardβπ))
β π))) |
59 | 55, 58 | mpdi 45 |
. . . . . . . . . . . . . . 15
β’ (π β Tarski β
((cardβπ) β
π β
((cfβ(cardβπ))
Γ (cardβπ))
β π)) |
60 | 52, 59 | mpd 15 |
. . . . . . . . . . . . . 14
β’ (π β Tarski β
((cfβ(cardβπ))
Γ (cardβπ))
β π) |
61 | | sstr2 3984 |
. . . . . . . . . . . . . 14
β’ (π₯ β
((cfβ(cardβπ))
Γ (cardβπ))
β (((cfβ(cardβπ)) Γ (cardβπ)) β π β π₯ β π)) |
62 | 50, 60, 61 | syl2im 40 |
. . . . . . . . . . . . 13
β’ (π₯ β ((cardβπ) βm
(cfβ(cardβπ)))
β (π β Tarski
β π₯ β π)) |
63 | 45, 44, 62 | sylc 65 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ) β§
π₯ β ((cardβπ) βm
(cfβ(cardβπ))))
β π₯ β π) |
64 | | simp2 1134 |
. . . . . . . . . . . . 13
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ) β§
π₯ β ((cardβπ) βm
(cfβ(cardβπ))))
β (cfβ(cardβπ)) β (cardβπ)) |
65 | | ffn 6710 |
. . . . . . . . . . . . . . . . 17
β’ (π₯:(cfβ(cardβπ))βΆ(cardβπ) β π₯ Fn (cfβ(cardβπ))) |
66 | | fndmeng 9034 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ Fn (cfβ(cardβπ)) β§
(cfβ(cardβπ))
β V) β (cfβ(cardβπ)) β π₯) |
67 | 65, 47, 66 | sylancl 585 |
. . . . . . . . . . . . . . . 16
β’ (π₯:(cfβ(cardβπ))βΆ(cardβπ) β
(cfβ(cardβπ))
β π₯) |
68 | 48, 67 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’ (π₯ β ((cardβπ) βm
(cfβ(cardβπ)))
β (cfβ(cardβπ)) β π₯) |
69 | 68 | ensymd 9000 |
. . . . . . . . . . . . . 14
β’ (π₯ β ((cardβπ) βm
(cfβ(cardβπ)))
β π₯ β
(cfβ(cardβπ))) |
70 | | cardsdomelir 9967 |
. . . . . . . . . . . . . 14
β’
((cfβ(cardβπ)) β (cardβπ) β (cfβ(cardβπ)) βΊ π) |
71 | | ensdomtr 9112 |
. . . . . . . . . . . . . 14
β’ ((π₯ β
(cfβ(cardβπ))
β§ (cfβ(cardβπ)) βΊ π) β π₯ βΊ π) |
72 | 69, 70, 71 | syl2an 595 |
. . . . . . . . . . . . 13
β’ ((π₯ β ((cardβπ) βm
(cfβ(cardβπ)))
β§ (cfβ(cardβπ)) β (cardβπ)) β π₯ βΊ π) |
73 | 45, 64, 72 | syl2anc 583 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ) β§
π₯ β ((cardβπ) βm
(cfβ(cardβπ))))
β π₯ βΊ π) |
74 | | tskssel 10751 |
. . . . . . . . . . . 12
β’ ((π β Tarski β§ π₯ β π β§ π₯ βΊ π) β π₯ β π) |
75 | 44, 63, 73, 74 | syl3anc 1368 |
. . . . . . . . . . 11
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ) β§
π₯ β ((cardβπ) βm
(cfβ(cardβπ))))
β π₯ β π) |
76 | 75 | 3expia 1118 |
. . . . . . . . . 10
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ))
β (π₯ β
((cardβπ)
βm (cfβ(cardβπ))) β π₯ β π)) |
77 | 76 | ssrdv 3983 |
. . . . . . . . 9
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ))
β ((cardβπ)
βm (cfβ(cardβπ))) β π) |
78 | | ssdomg 8995 |
. . . . . . . . . 10
β’ (π β Tarski β
(((cardβπ)
βm (cfβ(cardβπ))) β π β ((cardβπ) βm
(cfβ(cardβπ)))
βΌ π)) |
79 | 78 | imp 406 |
. . . . . . . . 9
β’ ((π β Tarski β§
((cardβπ)
βm (cfβ(cardβπ))) β π) β ((cardβπ) βm
(cfβ(cardβπ)))
βΌ π) |
80 | 77, 79 | syldan 590 |
. . . . . . . 8
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ))
β ((cardβπ)
βm (cfβ(cardβπ))) βΌ π) |
81 | 23 | adantr 480 |
. . . . . . . 8
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ))
β π β
(cardβπ)) |
82 | | domentr 9008 |
. . . . . . . 8
β’
((((cardβπ)
βm (cfβ(cardβπ))) βΌ π β§ π β (cardβπ)) β ((cardβπ) βm
(cfβ(cardβπ)))
βΌ (cardβπ)) |
83 | 80, 81, 82 | syl2anc 583 |
. . . . . . 7
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ))
β ((cardβπ)
βm (cfβ(cardβπ))) βΌ (cardβπ)) |
84 | | domnsym 9098 |
. . . . . . 7
β’
(((cardβπ)
βm (cfβ(cardβπ))) βΌ (cardβπ) β Β¬ (cardβπ) βΊ ((cardβπ) βm
(cfβ(cardβπ)))) |
85 | 83, 84 | syl 17 |
. . . . . 6
β’ ((π β Tarski β§
(cfβ(cardβπ))
β (cardβπ))
β Β¬ (cardβπ)
βΊ ((cardβπ)
βm (cfβ(cardβπ)))) |
86 | 85 | ex 412 |
. . . . 5
β’ (π β Tarski β
((cfβ(cardβπ))
β (cardβπ)
β Β¬ (cardβπ)
βΊ ((cardβπ)
βm (cfβ(cardβπ))))) |
87 | 86 | adantr 480 |
. . . 4
β’ ((π β Tarski β§ π β β
) β
((cfβ(cardβπ))
β (cardβπ)
β Β¬ (cardβπ)
βΊ ((cardβπ)
βm (cfβ(cardβπ))))) |
88 | 43, 87 | mt2d 136 |
. . 3
β’ ((π β Tarski β§ π β β
) β Β¬
(cfβ(cardβπ))
β (cardβπ)) |
89 | | cfon 10249 |
. . . . . 6
β’
(cfβ(cardβπ)) β On |
90 | 89, 9 | onsseli 6478 |
. . . . 5
β’
((cfβ(cardβπ)) β (cardβπ) β ((cfβ(cardβπ)) β (cardβπ) β¨
(cfβ(cardβπ)) =
(cardβπ))) |
91 | 53, 90 | mpbi 229 |
. . . 4
β’
((cfβ(cardβπ)) β (cardβπ) β¨ (cfβ(cardβπ)) = (cardβπ)) |
92 | 91 | ori 858 |
. . 3
β’ (Β¬
(cfβ(cardβπ))
β (cardβπ)
β (cfβ(cardβπ)) = (cardβπ)) |
93 | 88, 92 | syl 17 |
. 2
β’ ((π β Tarski β§ π β β
) β
(cfβ(cardβπ)) =
(cardβπ)) |
94 | | elina 10681 |
. 2
β’
((cardβπ)
β Inacc β ((cardβπ) β β
β§
(cfβ(cardβπ)) =
(cardβπ) β§
βπ₯ β
(cardβπ)π«
π₯ βΊ (cardβπ))) |
95 | 3, 93, 30, 94 | syl3anbrc 1340 |
1
β’ ((π β Tarski β§ π β β
) β
(cardβπ) β
Inacc) |