MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rankcf Structured version   Visualization version   GIF version

Theorem rankcf 10772
Description: Any set must be at least as large as the cofinality of its rank, because the ranks of the elements of 𝐴 form a cofinal map into (rankβ€˜π΄). (Contributed by Mario Carneiro, 27-May-2013.)
Assertion
Ref Expression
rankcf Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄))

Proof of Theorem rankcf
Dummy variables 𝑀 π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rankon 9790 . . 3 (rankβ€˜π΄) ∈ On
2 onzsl 7835 . . 3 ((rankβ€˜π΄) ∈ On ↔ ((rankβ€˜π΄) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜π΄) = suc π‘₯ ∨ ((rankβ€˜π΄) ∈ V ∧ Lim (rankβ€˜π΄))))
31, 2mpbi 229 . 2 ((rankβ€˜π΄) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜π΄) = suc π‘₯ ∨ ((rankβ€˜π΄) ∈ V ∧ Lim (rankβ€˜π΄)))
4 sdom0 9108 . . . 4 Β¬ 𝐴 β‰Ί βˆ…
5 fveq2 6892 . . . . . 6 ((rankβ€˜π΄) = βˆ… β†’ (cfβ€˜(rankβ€˜π΄)) = (cfβ€˜βˆ…))
6 cf0 10246 . . . . . 6 (cfβ€˜βˆ…) = βˆ…
75, 6eqtrdi 2789 . . . . 5 ((rankβ€˜π΄) = βˆ… β†’ (cfβ€˜(rankβ€˜π΄)) = βˆ…)
87breq2d 5161 . . . 4 ((rankβ€˜π΄) = βˆ… β†’ (𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)) ↔ 𝐴 β‰Ί βˆ…))
94, 8mtbiri 327 . . 3 ((rankβ€˜π΄) = βˆ… β†’ Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)))
10 fveq2 6892 . . . . . . 7 ((rankβ€˜π΄) = suc π‘₯ β†’ (cfβ€˜(rankβ€˜π΄)) = (cfβ€˜suc π‘₯))
11 cfsuc 10252 . . . . . . 7 (π‘₯ ∈ On β†’ (cfβ€˜suc π‘₯) = 1o)
1210, 11sylan9eqr 2795 . . . . . 6 ((π‘₯ ∈ On ∧ (rankβ€˜π΄) = suc π‘₯) β†’ (cfβ€˜(rankβ€˜π΄)) = 1o)
13 nsuceq0 6448 . . . . . . . . 9 suc π‘₯ β‰  βˆ…
14 neeq1 3004 . . . . . . . . 9 ((rankβ€˜π΄) = suc π‘₯ β†’ ((rankβ€˜π΄) β‰  βˆ… ↔ suc π‘₯ β‰  βˆ…))
1513, 14mpbiri 258 . . . . . . . 8 ((rankβ€˜π΄) = suc π‘₯ β†’ (rankβ€˜π΄) β‰  βˆ…)
16 fveq2 6892 . . . . . . . . . . 11 (𝐴 = βˆ… β†’ (rankβ€˜π΄) = (rankβ€˜βˆ…))
17 0elon 6419 . . . . . . . . . . . . 13 βˆ… ∈ On
18 r1fnon 9762 . . . . . . . . . . . . . 14 𝑅1 Fn On
1918fndmi 6654 . . . . . . . . . . . . 13 dom 𝑅1 = On
2017, 19eleqtrri 2833 . . . . . . . . . . . 12 βˆ… ∈ dom 𝑅1
21 rankonid 9824 . . . . . . . . . . . 12 (βˆ… ∈ dom 𝑅1 ↔ (rankβ€˜βˆ…) = βˆ…)
2220, 21mpbi 229 . . . . . . . . . . 11 (rankβ€˜βˆ…) = βˆ…
2316, 22eqtrdi 2789 . . . . . . . . . 10 (𝐴 = βˆ… β†’ (rankβ€˜π΄) = βˆ…)
2423necon3i 2974 . . . . . . . . 9 ((rankβ€˜π΄) β‰  βˆ… β†’ 𝐴 β‰  βˆ…)
25 rankvaln 9794 . . . . . . . . . . 11 (Β¬ 𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ (rankβ€˜π΄) = βˆ…)
2625necon1ai 2969 . . . . . . . . . 10 ((rankβ€˜π΄) β‰  βˆ… β†’ 𝐴 ∈ βˆͺ (𝑅1 β€œ On))
27 breq2 5153 . . . . . . . . . . 11 (𝑦 = 𝐴 β†’ (1o β‰Ό 𝑦 ↔ 1o β‰Ό 𝐴))
28 neeq1 3004 . . . . . . . . . . 11 (𝑦 = 𝐴 β†’ (𝑦 β‰  βˆ… ↔ 𝐴 β‰  βˆ…))
29 0sdom1dom 9238 . . . . . . . . . . . 12 (βˆ… β‰Ί 𝑦 ↔ 1o β‰Ό 𝑦)
30 vex 3479 . . . . . . . . . . . . 13 𝑦 ∈ V
31300sdom 9107 . . . . . . . . . . . 12 (βˆ… β‰Ί 𝑦 ↔ 𝑦 β‰  βˆ…)
3229, 31bitr3i 277 . . . . . . . . . . 11 (1o β‰Ό 𝑦 ↔ 𝑦 β‰  βˆ…)
3327, 28, 32vtoclbg 3560 . . . . . . . . . 10 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ (1o β‰Ό 𝐴 ↔ 𝐴 β‰  βˆ…))
3426, 33syl 17 . . . . . . . . 9 ((rankβ€˜π΄) β‰  βˆ… β†’ (1o β‰Ό 𝐴 ↔ 𝐴 β‰  βˆ…))
3524, 34mpbird 257 . . . . . . . 8 ((rankβ€˜π΄) β‰  βˆ… β†’ 1o β‰Ό 𝐴)
3615, 35syl 17 . . . . . . 7 ((rankβ€˜π΄) = suc π‘₯ β†’ 1o β‰Ό 𝐴)
3736adantl 483 . . . . . 6 ((π‘₯ ∈ On ∧ (rankβ€˜π΄) = suc π‘₯) β†’ 1o β‰Ό 𝐴)
3812, 37eqbrtrd 5171 . . . . 5 ((π‘₯ ∈ On ∧ (rankβ€˜π΄) = suc π‘₯) β†’ (cfβ€˜(rankβ€˜π΄)) β‰Ό 𝐴)
3938rexlimiva 3148 . . . 4 (βˆƒπ‘₯ ∈ On (rankβ€˜π΄) = suc π‘₯ β†’ (cfβ€˜(rankβ€˜π΄)) β‰Ό 𝐴)
40 domnsym 9099 . . . 4 ((cfβ€˜(rankβ€˜π΄)) β‰Ό 𝐴 β†’ Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)))
4139, 40syl 17 . . 3 (βˆƒπ‘₯ ∈ On (rankβ€˜π΄) = suc π‘₯ β†’ Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)))
42 nlim0 6424 . . . . . . . . . . . . . . . . 17 Β¬ Lim βˆ…
43 limeq 6377 . . . . . . . . . . . . . . . . 17 ((rankβ€˜π΄) = βˆ… β†’ (Lim (rankβ€˜π΄) ↔ Lim βˆ…))
4442, 43mtbiri 327 . . . . . . . . . . . . . . . 16 ((rankβ€˜π΄) = βˆ… β†’ Β¬ Lim (rankβ€˜π΄))
4525, 44syl 17 . . . . . . . . . . . . . . 15 (Β¬ 𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ Β¬ Lim (rankβ€˜π΄))
4645con4i 114 . . . . . . . . . . . . . 14 (Lim (rankβ€˜π΄) β†’ 𝐴 ∈ βˆͺ (𝑅1 β€œ On))
47 r1elssi 9800 . . . . . . . . . . . . . 14 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝐴 βŠ† βˆͺ (𝑅1 β€œ On))
4846, 47syl 17 . . . . . . . . . . . . 13 (Lim (rankβ€˜π΄) β†’ 𝐴 βŠ† βˆͺ (𝑅1 β€œ On))
4948sselda 3983 . . . . . . . . . . . 12 ((Lim (rankβ€˜π΄) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ βˆͺ (𝑅1 β€œ On))
50 ranksnb 9822 . . . . . . . . . . . 12 (π‘₯ ∈ βˆͺ (𝑅1 β€œ On) β†’ (rankβ€˜{π‘₯}) = suc (rankβ€˜π‘₯))
5149, 50syl 17 . . . . . . . . . . 11 ((Lim (rankβ€˜π΄) ∧ π‘₯ ∈ 𝐴) β†’ (rankβ€˜{π‘₯}) = suc (rankβ€˜π‘₯))
52 rankelb 9819 . . . . . . . . . . . . . 14 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ (π‘₯ ∈ 𝐴 β†’ (rankβ€˜π‘₯) ∈ (rankβ€˜π΄)))
5346, 52syl 17 . . . . . . . . . . . . 13 (Lim (rankβ€˜π΄) β†’ (π‘₯ ∈ 𝐴 β†’ (rankβ€˜π‘₯) ∈ (rankβ€˜π΄)))
54 limsuc 7838 . . . . . . . . . . . . 13 (Lim (rankβ€˜π΄) β†’ ((rankβ€˜π‘₯) ∈ (rankβ€˜π΄) ↔ suc (rankβ€˜π‘₯) ∈ (rankβ€˜π΄)))
5553, 54sylibd 238 . . . . . . . . . . . 12 (Lim (rankβ€˜π΄) β†’ (π‘₯ ∈ 𝐴 β†’ suc (rankβ€˜π‘₯) ∈ (rankβ€˜π΄)))
5655imp 408 . . . . . . . . . . 11 ((Lim (rankβ€˜π΄) ∧ π‘₯ ∈ 𝐴) β†’ suc (rankβ€˜π‘₯) ∈ (rankβ€˜π΄))
5751, 56eqeltrd 2834 . . . . . . . . . 10 ((Lim (rankβ€˜π΄) ∧ π‘₯ ∈ 𝐴) β†’ (rankβ€˜{π‘₯}) ∈ (rankβ€˜π΄))
58 eleq1a 2829 . . . . . . . . . 10 ((rankβ€˜{π‘₯}) ∈ (rankβ€˜π΄) β†’ (𝑀 = (rankβ€˜{π‘₯}) β†’ 𝑀 ∈ (rankβ€˜π΄)))
5957, 58syl 17 . . . . . . . . 9 ((Lim (rankβ€˜π΄) ∧ π‘₯ ∈ 𝐴) β†’ (𝑀 = (rankβ€˜{π‘₯}) β†’ 𝑀 ∈ (rankβ€˜π΄)))
6059rexlimdva 3156 . . . . . . . 8 (Lim (rankβ€˜π΄) β†’ (βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯}) β†’ 𝑀 ∈ (rankβ€˜π΄)))
6160abssdv 4066 . . . . . . 7 (Lim (rankβ€˜π΄) β†’ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} βŠ† (rankβ€˜π΄))
62 vsnex 5430 . . . . . . . . . . . . 13 {π‘₯} ∈ V
6362dfiun2 5037 . . . . . . . . . . . 12 βˆͺ π‘₯ ∈ 𝐴 {π‘₯} = βˆͺ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}}
64 iunid 5064 . . . . . . . . . . . 12 βˆͺ π‘₯ ∈ 𝐴 {π‘₯} = 𝐴
6563, 64eqtr3i 2763 . . . . . . . . . . 11 βˆͺ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} = 𝐴
6665fveq2i 6895 . . . . . . . . . 10 (rankβ€˜βˆͺ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}}) = (rankβ€˜π΄)
6747sselda 3983 . . . . . . . . . . . . . . 15 ((𝐴 ∈ βˆͺ (𝑅1 β€œ On) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ βˆͺ (𝑅1 β€œ On))
68 snwf 9804 . . . . . . . . . . . . . . 15 (π‘₯ ∈ βˆͺ (𝑅1 β€œ On) β†’ {π‘₯} ∈ βˆͺ (𝑅1 β€œ On))
69 eleq1a 2829 . . . . . . . . . . . . . . 15 ({π‘₯} ∈ βˆͺ (𝑅1 β€œ On) β†’ (𝑦 = {π‘₯} β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On)))
7067, 68, 693syl 18 . . . . . . . . . . . . . 14 ((𝐴 ∈ βˆͺ (𝑅1 β€œ On) ∧ π‘₯ ∈ 𝐴) β†’ (𝑦 = {π‘₯} β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On)))
7170rexlimdva 3156 . . . . . . . . . . . . 13 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ (βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯} β†’ 𝑦 ∈ βˆͺ (𝑅1 β€œ On)))
7271abssdv 4066 . . . . . . . . . . . 12 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} βŠ† βˆͺ (𝑅1 β€œ On))
73 abrexexg 7947 . . . . . . . . . . . . 13 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} ∈ V)
74 eleq1 2822 . . . . . . . . . . . . . 14 (𝑧 = {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} β†’ (𝑧 ∈ βˆͺ (𝑅1 β€œ On) ↔ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} ∈ βˆͺ (𝑅1 β€œ On)))
75 sseq1 4008 . . . . . . . . . . . . . 14 (𝑧 = {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} β†’ (𝑧 βŠ† βˆͺ (𝑅1 β€œ On) ↔ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} βŠ† βˆͺ (𝑅1 β€œ On)))
76 vex 3479 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7776r1elss 9801 . . . . . . . . . . . . . 14 (𝑧 ∈ βˆͺ (𝑅1 β€œ On) ↔ 𝑧 βŠ† βˆͺ (𝑅1 β€œ On))
7874, 75, 77vtoclbg 3560 . . . . . . . . . . . . 13 ({𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} ∈ V β†’ ({𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} ∈ βˆͺ (𝑅1 β€œ On) ↔ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} βŠ† βˆͺ (𝑅1 β€œ On)))
7973, 78syl 17 . . . . . . . . . . . 12 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ ({𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} ∈ βˆͺ (𝑅1 β€œ On) ↔ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} βŠ† βˆͺ (𝑅1 β€œ On)))
8072, 79mpbird 257 . . . . . . . . . . 11 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} ∈ βˆͺ (𝑅1 β€œ On))
81 rankuni2b 9848 . . . . . . . . . . 11 ({𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} ∈ βˆͺ (𝑅1 β€œ On) β†’ (rankβ€˜βˆͺ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}}) = βˆͺ 𝑧 ∈ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} (rankβ€˜π‘§))
8280, 81syl 17 . . . . . . . . . 10 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ (rankβ€˜βˆͺ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}}) = βˆͺ 𝑧 ∈ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} (rankβ€˜π‘§))
8366, 82eqtr3id 2787 . . . . . . . . 9 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ (rankβ€˜π΄) = βˆͺ 𝑧 ∈ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} (rankβ€˜π‘§))
84 fvex 6905 . . . . . . . . . . 11 (rankβ€˜π‘§) ∈ V
8584dfiun2 5037 . . . . . . . . . 10 βˆͺ 𝑧 ∈ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} (rankβ€˜π‘§) = βˆͺ {𝑀 ∣ βˆƒπ‘§ ∈ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}}𝑀 = (rankβ€˜π‘§)}
86 fveq2 6892 . . . . . . . . . . . 12 (𝑧 = {π‘₯} β†’ (rankβ€˜π‘§) = (rankβ€˜{π‘₯}))
8762, 86abrexco 7243 . . . . . . . . . . 11 {𝑀 ∣ βˆƒπ‘§ ∈ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}}𝑀 = (rankβ€˜π‘§)} = {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})}
8887unieqi 4922 . . . . . . . . . 10 βˆͺ {𝑀 ∣ βˆƒπ‘§ ∈ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}}𝑀 = (rankβ€˜π‘§)} = βˆͺ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})}
8985, 88eqtri 2761 . . . . . . . . 9 βˆͺ 𝑧 ∈ {𝑦 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑦 = {π‘₯}} (rankβ€˜π‘§) = βˆͺ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})}
9083, 89eqtr2di 2790 . . . . . . . 8 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ βˆͺ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} = (rankβ€˜π΄))
9146, 90syl 17 . . . . . . 7 (Lim (rankβ€˜π΄) β†’ βˆͺ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} = (rankβ€˜π΄))
92 fvex 6905 . . . . . . . 8 (rankβ€˜π΄) ∈ V
9392cfslb 10261 . . . . . . 7 ((Lim (rankβ€˜π΄) ∧ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} βŠ† (rankβ€˜π΄) ∧ βˆͺ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} = (rankβ€˜π΄)) β†’ (cfβ€˜(rankβ€˜π΄)) β‰Ό {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})})
9461, 91, 93mpd3an23 1464 . . . . . 6 (Lim (rankβ€˜π΄) β†’ (cfβ€˜(rankβ€˜π΄)) β‰Ό {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})})
95 2fveq3 6897 . . . . . . . . . 10 (𝑦 = 𝐴 β†’ (cfβ€˜(rankβ€˜π‘¦)) = (cfβ€˜(rankβ€˜π΄)))
96 breq12 5154 . . . . . . . . . 10 ((𝑦 = 𝐴 ∧ (cfβ€˜(rankβ€˜π‘¦)) = (cfβ€˜(rankβ€˜π΄))) β†’ (𝑦 β‰Ί (cfβ€˜(rankβ€˜π‘¦)) ↔ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄))))
9795, 96mpdan 686 . . . . . . . . 9 (𝑦 = 𝐴 β†’ (𝑦 β‰Ί (cfβ€˜(rankβ€˜π‘¦)) ↔ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄))))
98 rexeq 3322 . . . . . . . . . . 11 (𝑦 = 𝐴 β†’ (βˆƒπ‘₯ ∈ 𝑦 𝑀 = (rankβ€˜{π‘₯}) ↔ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})))
9998abbidv 2802 . . . . . . . . . 10 (𝑦 = 𝐴 β†’ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝑦 𝑀 = (rankβ€˜{π‘₯})} = {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})})
100 breq12 5154 . . . . . . . . . 10 (({𝑀 ∣ βˆƒπ‘₯ ∈ 𝑦 𝑀 = (rankβ€˜{π‘₯})} = {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} ∧ 𝑦 = 𝐴) β†’ ({𝑀 ∣ βˆƒπ‘₯ ∈ 𝑦 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝑦 ↔ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝐴))
10199, 100mpancom 687 . . . . . . . . 9 (𝑦 = 𝐴 β†’ ({𝑀 ∣ βˆƒπ‘₯ ∈ 𝑦 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝑦 ↔ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝐴))
10297, 101imbi12d 345 . . . . . . . 8 (𝑦 = 𝐴 β†’ ((𝑦 β‰Ί (cfβ€˜(rankβ€˜π‘¦)) β†’ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝑦 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝑦) ↔ (𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)) β†’ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝐴)))
103 eqid 2733 . . . . . . . . . 10 (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})) = (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯}))
104103rnmpt 5955 . . . . . . . . 9 ran (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})) = {𝑀 ∣ βˆƒπ‘₯ ∈ 𝑦 𝑀 = (rankβ€˜{π‘₯})}
105 cfon 10250 . . . . . . . . . . 11 (cfβ€˜(rankβ€˜π‘¦)) ∈ On
106 sdomdom 8976 . . . . . . . . . . 11 (𝑦 β‰Ί (cfβ€˜(rankβ€˜π‘¦)) β†’ 𝑦 β‰Ό (cfβ€˜(rankβ€˜π‘¦)))
107 ondomen 10032 . . . . . . . . . . 11 (((cfβ€˜(rankβ€˜π‘¦)) ∈ On ∧ 𝑦 β‰Ό (cfβ€˜(rankβ€˜π‘¦))) β†’ 𝑦 ∈ dom card)
108105, 106, 107sylancr 588 . . . . . . . . . 10 (𝑦 β‰Ί (cfβ€˜(rankβ€˜π‘¦)) β†’ 𝑦 ∈ dom card)
109 fvex 6905 . . . . . . . . . . . 12 (rankβ€˜{π‘₯}) ∈ V
110109, 103fnmpti 6694 . . . . . . . . . . 11 (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})) Fn 𝑦
111 dffn4 6812 . . . . . . . . . . 11 ((π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})) Fn 𝑦 ↔ (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})):𝑦–ontoβ†’ran (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})))
112110, 111mpbi 229 . . . . . . . . . 10 (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})):𝑦–ontoβ†’ran (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯}))
113 fodomnum 10052 . . . . . . . . . 10 (𝑦 ∈ dom card β†’ ((π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})):𝑦–ontoβ†’ran (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})) β†’ ran (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})) β‰Ό 𝑦))
114108, 112, 113mpisyl 21 . . . . . . . . 9 (𝑦 β‰Ί (cfβ€˜(rankβ€˜π‘¦)) β†’ ran (π‘₯ ∈ 𝑦 ↦ (rankβ€˜{π‘₯})) β‰Ό 𝑦)
115104, 114eqbrtrrid 5185 . . . . . . . 8 (𝑦 β‰Ί (cfβ€˜(rankβ€˜π‘¦)) β†’ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝑦 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝑦)
116102, 115vtoclg 3557 . . . . . . 7 (𝐴 ∈ βˆͺ (𝑅1 β€œ On) β†’ (𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)) β†’ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝐴))
11746, 116syl 17 . . . . . 6 (Lim (rankβ€˜π΄) β†’ (𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)) β†’ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝐴))
118 domtr 9003 . . . . . . 7 (((cfβ€˜(rankβ€˜π΄)) β‰Ό {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} ∧ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝐴) β†’ (cfβ€˜(rankβ€˜π΄)) β‰Ό 𝐴)
119118, 40syl 17 . . . . . 6 (((cfβ€˜(rankβ€˜π΄)) β‰Ό {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} ∧ {𝑀 ∣ βˆƒπ‘₯ ∈ 𝐴 𝑀 = (rankβ€˜{π‘₯})} β‰Ό 𝐴) β†’ Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)))
12094, 117, 119syl6an 683 . . . . 5 (Lim (rankβ€˜π΄) β†’ (𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)) β†’ Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄))))
121120pm2.01d 189 . . . 4 (Lim (rankβ€˜π΄) β†’ Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)))
122121adantl 483 . . 3 (((rankβ€˜π΄) ∈ V ∧ Lim (rankβ€˜π΄)) β†’ Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)))
1239, 41, 1223jaoi 1428 . 2 (((rankβ€˜π΄) = βˆ… ∨ βˆƒπ‘₯ ∈ On (rankβ€˜π΄) = suc π‘₯ ∨ ((rankβ€˜π΄) ∈ V ∧ Lim (rankβ€˜π΄))) β†’ Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄)))
1243, 123ax-mp 5 1 Β¬ 𝐴 β‰Ί (cfβ€˜(rankβ€˜π΄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ w3o 1087   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆƒwrex 3071  Vcvv 3475   βŠ† wss 3949  βˆ…c0 4323  {csn 4629  βˆͺ cuni 4909  βˆͺ ciun 4998   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677  ran crn 5678   β€œ cima 5680  Oncon0 6365  Lim wlim 6366  suc csuc 6367   Fn wfn 6539  β€“ontoβ†’wfo 6542  β€˜cfv 6544  1oc1o 8459   β‰Ό cdom 8937   β‰Ί csdm 8938  π‘…1cr1 9757  rankcrnk 9758  cardccrd 9930  cfccf 9932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-r1 9759  df-rank 9760  df-card 9934  df-cf 9936  df-acn 9937
This theorem is referenced by:  inatsk  10773  grur1  10815
  Copyright terms: Public domain W3C validator