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

Theorem rankcf 9880
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 8901 . . 3 (rank‘𝐴) ∈ On
2 onzsl 7272 . . 3 ((rank‘𝐴) ∈ On ↔ ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴))))
31, 2mpbi 221 . 2 ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)))
4 sdom0 8327 . . . 4 ¬ 𝐴 ≺ ∅
5 fveq2 6404 . . . . . 6 ((rank‘𝐴) = ∅ → (cf‘(rank‘𝐴)) = (cf‘∅))
6 cf0 9354 . . . . . 6 (cf‘∅) = ∅
75, 6syl6eq 2856 . . . . 5 ((rank‘𝐴) = ∅ → (cf‘(rank‘𝐴)) = ∅)
87breq2d 4856 . . . 4 ((rank‘𝐴) = ∅ → (𝐴 ≺ (cf‘(rank‘𝐴)) ↔ 𝐴 ≺ ∅))
94, 8mtbiri 318 . . 3 ((rank‘𝐴) = ∅ → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
10 fveq2 6404 . . . . . . 7 ((rank‘𝐴) = suc 𝑥 → (cf‘(rank‘𝐴)) = (cf‘suc 𝑥))
11 cfsuc 9360 . . . . . . 7 (𝑥 ∈ On → (cf‘suc 𝑥) = 1𝑜)
1210, 11sylan9eqr 2862 . . . . . 6 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → (cf‘(rank‘𝐴)) = 1𝑜)
13 nsuceq0 6017 . . . . . . . . 9 suc 𝑥 ≠ ∅
14 neeq1 3040 . . . . . . . . 9 ((rank‘𝐴) = suc 𝑥 → ((rank‘𝐴) ≠ ∅ ↔ suc 𝑥 ≠ ∅))
1513, 14mpbiri 249 . . . . . . . 8 ((rank‘𝐴) = suc 𝑥 → (rank‘𝐴) ≠ ∅)
16 fveq2 6404 . . . . . . . . . . 11 (𝐴 = ∅ → (rank‘𝐴) = (rank‘∅))
17 0elon 5990 . . . . . . . . . . . . 13 ∅ ∈ On
18 r1fnon 8873 . . . . . . . . . . . . . 14 𝑅1 Fn On
19 fndm 6197 . . . . . . . . . . . . . 14 (𝑅1 Fn On → dom 𝑅1 = On)
2018, 19ax-mp 5 . . . . . . . . . . . . 13 dom 𝑅1 = On
2117, 20eleqtrri 2884 . . . . . . . . . . . 12 ∅ ∈ dom 𝑅1
22 rankonid 8935 . . . . . . . . . . . 12 (∅ ∈ dom 𝑅1 ↔ (rank‘∅) = ∅)
2321, 22mpbi 221 . . . . . . . . . . 11 (rank‘∅) = ∅
2416, 23syl6eq 2856 . . . . . . . . . 10 (𝐴 = ∅ → (rank‘𝐴) = ∅)
2524necon3i 3010 . . . . . . . . 9 ((rank‘𝐴) ≠ ∅ → 𝐴 ≠ ∅)
26 rankvaln 8905 . . . . . . . . . . 11 𝐴 (𝑅1 “ On) → (rank‘𝐴) = ∅)
2726necon1ai 3005 . . . . . . . . . 10 ((rank‘𝐴) ≠ ∅ → 𝐴 (𝑅1 “ On))
28 breq2 4848 . . . . . . . . . . 11 (𝑦 = 𝐴 → (1𝑜𝑦 ↔ 1𝑜𝐴))
29 neeq1 3040 . . . . . . . . . . 11 (𝑦 = 𝐴 → (𝑦 ≠ ∅ ↔ 𝐴 ≠ ∅))
30 0sdom1dom 8393 . . . . . . . . . . . 12 (∅ ≺ 𝑦 ↔ 1𝑜𝑦)
31 vex 3394 . . . . . . . . . . . . 13 𝑦 ∈ V
32310sdom 8326 . . . . . . . . . . . 12 (∅ ≺ 𝑦𝑦 ≠ ∅)
3330, 32bitr3i 268 . . . . . . . . . . 11 (1𝑜𝑦𝑦 ≠ ∅)
3428, 29, 33vtoclbg 3460 . . . . . . . . . 10 (𝐴 (𝑅1 “ On) → (1𝑜𝐴𝐴 ≠ ∅))
3527, 34syl 17 . . . . . . . . 9 ((rank‘𝐴) ≠ ∅ → (1𝑜𝐴𝐴 ≠ ∅))
3625, 35mpbird 248 . . . . . . . 8 ((rank‘𝐴) ≠ ∅ → 1𝑜𝐴)
3715, 36syl 17 . . . . . . 7 ((rank‘𝐴) = suc 𝑥 → 1𝑜𝐴)
3837adantl 469 . . . . . 6 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → 1𝑜𝐴)
3912, 38eqbrtrd 4866 . . . . 5 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → (cf‘(rank‘𝐴)) ≼ 𝐴)
4039rexlimiva 3216 . . . 4 (∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 → (cf‘(rank‘𝐴)) ≼ 𝐴)
41 domnsym 8321 . . . 4 ((cf‘(rank‘𝐴)) ≼ 𝐴 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
4240, 41syl 17 . . 3 (∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
43 nlim0 5995 . . . . . . . . . . . . . . . . 17 ¬ Lim ∅
44 limeq 5948 . . . . . . . . . . . . . . . . 17 ((rank‘𝐴) = ∅ → (Lim (rank‘𝐴) ↔ Lim ∅))
4543, 44mtbiri 318 . . . . . . . . . . . . . . . 16 ((rank‘𝐴) = ∅ → ¬ Lim (rank‘𝐴))
4626, 45syl 17 . . . . . . . . . . . . . . 15 𝐴 (𝑅1 “ On) → ¬ Lim (rank‘𝐴))
4746con4i 114 . . . . . . . . . . . . . 14 (Lim (rank‘𝐴) → 𝐴 (𝑅1 “ On))
48 r1elssi 8911 . . . . . . . . . . . . . 14 (𝐴 (𝑅1 “ On) → 𝐴 (𝑅1 “ On))
4947, 48syl 17 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → 𝐴 (𝑅1 “ On))
5049sselda 3798 . . . . . . . . . . . 12 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → 𝑥 (𝑅1 “ On))
51 ranksnb 8933 . . . . . . . . . . . 12 (𝑥 (𝑅1 “ On) → (rank‘{𝑥}) = suc (rank‘𝑥))
5250, 51syl 17 . . . . . . . . . . 11 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (rank‘{𝑥}) = suc (rank‘𝑥))
53 rankelb 8930 . . . . . . . . . . . . . 14 (𝐴 (𝑅1 “ On) → (𝑥𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
5447, 53syl 17 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → (𝑥𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
55 limsuc 7275 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → ((rank‘𝑥) ∈ (rank‘𝐴) ↔ suc (rank‘𝑥) ∈ (rank‘𝐴)))
5654, 55sylibd 230 . . . . . . . . . . . 12 (Lim (rank‘𝐴) → (𝑥𝐴 → suc (rank‘𝑥) ∈ (rank‘𝐴)))
5756imp 395 . . . . . . . . . . 11 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → suc (rank‘𝑥) ∈ (rank‘𝐴))
5852, 57eqeltrd 2885 . . . . . . . . . 10 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (rank‘{𝑥}) ∈ (rank‘𝐴))
59 eleq1a 2880 . . . . . . . . . 10 ((rank‘{𝑥}) ∈ (rank‘𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6058, 59syl 17 . . . . . . . . 9 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6160rexlimdva 3219 . . . . . . . 8 (Lim (rank‘𝐴) → (∃𝑥𝐴 𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6261abssdv 3873 . . . . . . 7 (Lim (rank‘𝐴) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴))
63 snex 5098 . . . . . . . . . . . . 13 {𝑥} ∈ V
6463dfiun2 4746 . . . . . . . . . . . 12 𝑥𝐴 {𝑥} = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}
65 iunid 4767 . . . . . . . . . . . 12 𝑥𝐴 {𝑥} = 𝐴
6664, 65eqtr3i 2830 . . . . . . . . . . 11 {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} = 𝐴
6766fveq2i 6407 . . . . . . . . . 10 (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = (rank‘𝐴)
6848sselda 3798 . . . . . . . . . . . . . . 15 ((𝐴 (𝑅1 “ On) ∧ 𝑥𝐴) → 𝑥 (𝑅1 “ On))
69 snwf 8915 . . . . . . . . . . . . . . 15 (𝑥 (𝑅1 “ On) → {𝑥} ∈ (𝑅1 “ On))
70 eleq1a 2880 . . . . . . . . . . . . . . 15 ({𝑥} ∈ (𝑅1 “ On) → (𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7168, 69, 703syl 18 . . . . . . . . . . . . . 14 ((𝐴 (𝑅1 “ On) ∧ 𝑥𝐴) → (𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7271rexlimdva 3219 . . . . . . . . . . . . 13 (𝐴 (𝑅1 “ On) → (∃𝑥𝐴 𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7372abssdv 3873 . . . . . . . . . . . 12 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On))
74 abrexexg 7366 . . . . . . . . . . . . 13 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ V)
75 eleq1 2873 . . . . . . . . . . . . . 14 (𝑧 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} → (𝑧 (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On)))
76 sseq1 3823 . . . . . . . . . . . . . 14 (𝑧 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} → (𝑧 (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
77 vex 3394 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7877r1elss 8912 . . . . . . . . . . . . . 14 (𝑧 (𝑅1 “ On) ↔ 𝑧 (𝑅1 “ On))
7975, 76, 78vtoclbg 3460 . . . . . . . . . . . . 13 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ V → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
8074, 79syl 17 . . . . . . . . . . . 12 (𝐴 (𝑅1 “ On) → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
8173, 80mpbird 248 . . . . . . . . . . 11 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On))
82 rankuni2b 8959 . . . . . . . . . . 11 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) → (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
8381, 82syl 17 . . . . . . . . . 10 (𝐴 (𝑅1 “ On) → (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
8467, 83syl5eqr 2854 . . . . . . . . 9 (𝐴 (𝑅1 “ On) → (rank‘𝐴) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
85 fvex 6417 . . . . . . . . . . 11 (rank‘𝑧) ∈ V
8685dfiun2 4746 . . . . . . . . . 10 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧) = {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)}
87 fveq2 6404 . . . . . . . . . . . 12 (𝑧 = {𝑥} → (rank‘𝑧) = (rank‘{𝑥}))
8863, 87abrexco 6722 . . . . . . . . . . 11 {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
8988unieqi 4639 . . . . . . . . . 10 {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
9086, 89eqtri 2828 . . . . . . . . 9 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧) = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
9184, 90syl6req 2857 . . . . . . . 8 (𝐴 (𝑅1 “ On) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴))
9247, 91syl 17 . . . . . . 7 (Lim (rank‘𝐴) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴))
93 fvex 6417 . . . . . . . 8 (rank‘𝐴) ∈ V
9493cfslb 9369 . . . . . . 7 ((Lim (rank‘𝐴) ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴) ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴)) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
9562, 92, 94mpd3an23 1580 . . . . . 6 (Lim (rank‘𝐴) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
96 2fveq3 6409 . . . . . . . . . 10 (𝑦 = 𝐴 → (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴)))
97 breq12 4849 . . . . . . . . . 10 ((𝑦 = 𝐴 ∧ (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴))) → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴))))
9896, 97mpdan 670 . . . . . . . . 9 (𝑦 = 𝐴 → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴))))
99 rexeq 3328 . . . . . . . . . . 11 (𝑦 = 𝐴 → (∃𝑥𝑦 𝑤 = (rank‘{𝑥}) ↔ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})))
10099abbidv 2925 . . . . . . . . . 10 (𝑦 = 𝐴 → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
101 breq12 4849 . . . . . . . . . 10 (({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ 𝑦 = 𝐴) → ({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
102100, 101mpancom 671 . . . . . . . . 9 (𝑦 = 𝐴 → ({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
10398, 102imbi12d 335 . . . . . . . 8 (𝑦 = 𝐴 → ((𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦) ↔ (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴)))
104 eqid 2806 . . . . . . . . . 10 (𝑥𝑦 ↦ (rank‘{𝑥})) = (𝑥𝑦 ↦ (rank‘{𝑥}))
105104rnmpt 5572 . . . . . . . . 9 ran (𝑥𝑦 ↦ (rank‘{𝑥})) = {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})}
106 cfon 9358 . . . . . . . . . . 11 (cf‘(rank‘𝑦)) ∈ On
107 sdomdom 8216 . . . . . . . . . . 11 (𝑦 ≺ (cf‘(rank‘𝑦)) → 𝑦 ≼ (cf‘(rank‘𝑦)))
108 ondomen 9139 . . . . . . . . . . 11 (((cf‘(rank‘𝑦)) ∈ On ∧ 𝑦 ≼ (cf‘(rank‘𝑦))) → 𝑦 ∈ dom card)
109106, 107, 108sylancr 577 . . . . . . . . . 10 (𝑦 ≺ (cf‘(rank‘𝑦)) → 𝑦 ∈ dom card)
110 fvex 6417 . . . . . . . . . . . 12 (rank‘{𝑥}) ∈ V
111110, 104fnmpti 6229 . . . . . . . . . . 11 (𝑥𝑦 ↦ (rank‘{𝑥})) Fn 𝑦
112 dffn4 6333 . . . . . . . . . . 11 ((𝑥𝑦 ↦ (rank‘{𝑥})) Fn 𝑦 ↔ (𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥})))
113111, 112mpbi 221 . . . . . . . . . 10 (𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥}))
114 fodomnum 9159 . . . . . . . . . 10 (𝑦 ∈ dom card → ((𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥})) → ran (𝑥𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦))
115109, 113, 114mpisyl 21 . . . . . . . . 9 (𝑦 ≺ (cf‘(rank‘𝑦)) → ran (𝑥𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦)
116105, 115syl5eqbrr 4880 . . . . . . . 8 (𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦)
117103, 116vtoclg 3459 . . . . . . 7 (𝐴 (𝑅1 “ On) → (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
11847, 117syl 17 . . . . . 6 (Lim (rank‘𝐴) → (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
119 domtr 8241 . . . . . . 7 (((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → (cf‘(rank‘𝐴)) ≼ 𝐴)
120119, 41syl 17 . . . . . 6 (((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
12195, 118, 120syl6an 666 . . . . 5 (Lim (rank‘𝐴) → (𝐴 ≺ (cf‘(rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴))))
122121pm2.01d 181 . . . 4 (Lim (rank‘𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
123122adantl 469 . . 3 (((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
1249, 42, 1233jaoi 1545 . 2 (((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴))) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
1253, 124ax-mp 5 1 ¬ 𝐴 ≺ (cf‘(rank‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3o 1099   = wceq 1637  wcel 2156  {cab 2792  wne 2978  wrex 3097  Vcvv 3391  wss 3769  c0 4116  {csn 4370   cuni 4630   ciun 4712   class class class wbr 4844  cmpt 4923  dom cdm 5311  ran crn 5312  cima 5314  Oncon0 5936  Lim wlim 5937  suc csuc 5938   Fn wfn 6092  ontowfo 6095  cfv 6097  1𝑜c1o 7785  cdom 8186  csdm 8187  𝑅1cr1 8868  rankcrnk 8869  cardccrd 9040  cfccf 9042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-er 7975  df-map 8090  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-r1 8870  df-rank 8871  df-card 9044  df-cf 9046  df-acn 9047
This theorem is referenced by:  inatsk  9881  grur1  9923
  Copyright terms: Public domain W3C validator