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

Theorem rankcf 9787
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 8827 . . 3 (rank‘𝐴) ∈ On
2 onzsl 7207 . . 3 ((rank‘𝐴) ∈ On ↔ ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴))))
31, 2mpbi 220 . 2 ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)))
4 sdom0 8253 . . . 4 ¬ 𝐴 ≺ ∅
5 fveq2 6348 . . . . . 6 ((rank‘𝐴) = ∅ → (cf‘(rank‘𝐴)) = (cf‘∅))
6 cf0 9261 . . . . . 6 (cf‘∅) = ∅
75, 6syl6eq 2806 . . . . 5 ((rank‘𝐴) = ∅ → (cf‘(rank‘𝐴)) = ∅)
87breq2d 4812 . . . 4 ((rank‘𝐴) = ∅ → (𝐴 ≺ (cf‘(rank‘𝐴)) ↔ 𝐴 ≺ ∅))
94, 8mtbiri 316 . . 3 ((rank‘𝐴) = ∅ → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
10 fveq2 6348 . . . . . . 7 ((rank‘𝐴) = suc 𝑥 → (cf‘(rank‘𝐴)) = (cf‘suc 𝑥))
11 cfsuc 9267 . . . . . . 7 (𝑥 ∈ On → (cf‘suc 𝑥) = 1𝑜)
1210, 11sylan9eqr 2812 . . . . . 6 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → (cf‘(rank‘𝐴)) = 1𝑜)
13 nsuceq0 5962 . . . . . . . . 9 suc 𝑥 ≠ ∅
14 neeq1 2990 . . . . . . . . 9 ((rank‘𝐴) = suc 𝑥 → ((rank‘𝐴) ≠ ∅ ↔ suc 𝑥 ≠ ∅))
1513, 14mpbiri 248 . . . . . . . 8 ((rank‘𝐴) = suc 𝑥 → (rank‘𝐴) ≠ ∅)
16 fveq2 6348 . . . . . . . . . . 11 (𝐴 = ∅ → (rank‘𝐴) = (rank‘∅))
17 0elon 5935 . . . . . . . . . . . . 13 ∅ ∈ On
18 r1fnon 8799 . . . . . . . . . . . . . 14 𝑅1 Fn On
19 fndm 6147 . . . . . . . . . . . . . 14 (𝑅1 Fn On → dom 𝑅1 = On)
2018, 19ax-mp 5 . . . . . . . . . . . . 13 dom 𝑅1 = On
2117, 20eleqtrri 2834 . . . . . . . . . . . 12 ∅ ∈ dom 𝑅1
22 rankonid 8861 . . . . . . . . . . . 12 (∅ ∈ dom 𝑅1 ↔ (rank‘∅) = ∅)
2321, 22mpbi 220 . . . . . . . . . . 11 (rank‘∅) = ∅
2416, 23syl6eq 2806 . . . . . . . . . 10 (𝐴 = ∅ → (rank‘𝐴) = ∅)
2524necon3i 2960 . . . . . . . . 9 ((rank‘𝐴) ≠ ∅ → 𝐴 ≠ ∅)
26 rankvaln 8831 . . . . . . . . . . 11 𝐴 (𝑅1 “ On) → (rank‘𝐴) = ∅)
2726necon1ai 2955 . . . . . . . . . 10 ((rank‘𝐴) ≠ ∅ → 𝐴 (𝑅1 “ On))
28 breq2 4804 . . . . . . . . . . 11 (𝑦 = 𝐴 → (1𝑜𝑦 ↔ 1𝑜𝐴))
29 neeq1 2990 . . . . . . . . . . 11 (𝑦 = 𝐴 → (𝑦 ≠ ∅ ↔ 𝐴 ≠ ∅))
30 0sdom1dom 8319 . . . . . . . . . . . 12 (∅ ≺ 𝑦 ↔ 1𝑜𝑦)
31 vex 3339 . . . . . . . . . . . . 13 𝑦 ∈ V
32310sdom 8252 . . . . . . . . . . . 12 (∅ ≺ 𝑦𝑦 ≠ ∅)
3330, 32bitr3i 266 . . . . . . . . . . 11 (1𝑜𝑦𝑦 ≠ ∅)
3428, 29, 33vtoclbg 3403 . . . . . . . . . 10 (𝐴 (𝑅1 “ On) → (1𝑜𝐴𝐴 ≠ ∅))
3527, 34syl 17 . . . . . . . . 9 ((rank‘𝐴) ≠ ∅ → (1𝑜𝐴𝐴 ≠ ∅))
3625, 35mpbird 247 . . . . . . . 8 ((rank‘𝐴) ≠ ∅ → 1𝑜𝐴)
3715, 36syl 17 . . . . . . 7 ((rank‘𝐴) = suc 𝑥 → 1𝑜𝐴)
3837adantl 473 . . . . . 6 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → 1𝑜𝐴)
3912, 38eqbrtrd 4822 . . . . 5 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → (cf‘(rank‘𝐴)) ≼ 𝐴)
4039rexlimiva 3162 . . . 4 (∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 → (cf‘(rank‘𝐴)) ≼ 𝐴)
41 domnsym 8247 . . . 4 ((cf‘(rank‘𝐴)) ≼ 𝐴 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
4240, 41syl 17 . . 3 (∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
43 nlim0 5940 . . . . . . . . . . . . . . . . 17 ¬ Lim ∅
44 limeq 5892 . . . . . . . . . . . . . . . . 17 ((rank‘𝐴) = ∅ → (Lim (rank‘𝐴) ↔ Lim ∅))
4543, 44mtbiri 316 . . . . . . . . . . . . . . . 16 ((rank‘𝐴) = ∅ → ¬ Lim (rank‘𝐴))
4626, 45syl 17 . . . . . . . . . . . . . . 15 𝐴 (𝑅1 “ On) → ¬ Lim (rank‘𝐴))
4746con4i 113 . . . . . . . . . . . . . 14 (Lim (rank‘𝐴) → 𝐴 (𝑅1 “ On))
48 r1elssi 8837 . . . . . . . . . . . . . 14 (𝐴 (𝑅1 “ On) → 𝐴 (𝑅1 “ On))
4947, 48syl 17 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → 𝐴 (𝑅1 “ On))
5049sselda 3740 . . . . . . . . . . . 12 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → 𝑥 (𝑅1 “ On))
51 ranksnb 8859 . . . . . . . . . . . 12 (𝑥 (𝑅1 “ On) → (rank‘{𝑥}) = suc (rank‘𝑥))
5250, 51syl 17 . . . . . . . . . . 11 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (rank‘{𝑥}) = suc (rank‘𝑥))
53 rankelb 8856 . . . . . . . . . . . . . 14 (𝐴 (𝑅1 “ On) → (𝑥𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
5447, 53syl 17 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → (𝑥𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
55 limsuc 7210 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → ((rank‘𝑥) ∈ (rank‘𝐴) ↔ suc (rank‘𝑥) ∈ (rank‘𝐴)))
5654, 55sylibd 229 . . . . . . . . . . . 12 (Lim (rank‘𝐴) → (𝑥𝐴 → suc (rank‘𝑥) ∈ (rank‘𝐴)))
5756imp 444 . . . . . . . . . . 11 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → suc (rank‘𝑥) ∈ (rank‘𝐴))
5852, 57eqeltrd 2835 . . . . . . . . . 10 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (rank‘{𝑥}) ∈ (rank‘𝐴))
59 eleq1a 2830 . . . . . . . . . 10 ((rank‘{𝑥}) ∈ (rank‘𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6058, 59syl 17 . . . . . . . . 9 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6160rexlimdva 3165 . . . . . . . 8 (Lim (rank‘𝐴) → (∃𝑥𝐴 𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6261abssdv 3813 . . . . . . 7 (Lim (rank‘𝐴) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴))
63 snex 5053 . . . . . . . . . . . . 13 {𝑥} ∈ V
6463dfiun2 4702 . . . . . . . . . . . 12 𝑥𝐴 {𝑥} = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}
65 iunid 4723 . . . . . . . . . . . 12 𝑥𝐴 {𝑥} = 𝐴
6664, 65eqtr3i 2780 . . . . . . . . . . 11 {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} = 𝐴
6766fveq2i 6351 . . . . . . . . . 10 (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = (rank‘𝐴)
6848sselda 3740 . . . . . . . . . . . . . . 15 ((𝐴 (𝑅1 “ On) ∧ 𝑥𝐴) → 𝑥 (𝑅1 “ On))
69 snwf 8841 . . . . . . . . . . . . . . 15 (𝑥 (𝑅1 “ On) → {𝑥} ∈ (𝑅1 “ On))
70 eleq1a 2830 . . . . . . . . . . . . . . 15 ({𝑥} ∈ (𝑅1 “ On) → (𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7168, 69, 703syl 18 . . . . . . . . . . . . . 14 ((𝐴 (𝑅1 “ On) ∧ 𝑥𝐴) → (𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7271rexlimdva 3165 . . . . . . . . . . . . 13 (𝐴 (𝑅1 “ On) → (∃𝑥𝐴 𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7372abssdv 3813 . . . . . . . . . . . 12 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On))
74 abrexexg 7301 . . . . . . . . . . . . 13 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ V)
75 eleq1 2823 . . . . . . . . . . . . . 14 (𝑧 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} → (𝑧 (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On)))
76 sseq1 3763 . . . . . . . . . . . . . 14 (𝑧 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} → (𝑧 (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
77 vex 3339 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7877r1elss 8838 . . . . . . . . . . . . . 14 (𝑧 (𝑅1 “ On) ↔ 𝑧 (𝑅1 “ On))
7975, 76, 78vtoclbg 3403 . . . . . . . . . . . . 13 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ V → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
8074, 79syl 17 . . . . . . . . . . . 12 (𝐴 (𝑅1 “ On) → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
8173, 80mpbird 247 . . . . . . . . . . 11 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On))
82 rankuni2b 8885 . . . . . . . . . . 11 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) → (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
8381, 82syl 17 . . . . . . . . . 10 (𝐴 (𝑅1 “ On) → (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
8467, 83syl5eqr 2804 . . . . . . . . 9 (𝐴 (𝑅1 “ On) → (rank‘𝐴) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
85 fvex 6358 . . . . . . . . . . 11 (rank‘𝑧) ∈ V
8685dfiun2 4702 . . . . . . . . . 10 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧) = {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)}
87 fveq2 6348 . . . . . . . . . . . 12 (𝑧 = {𝑥} → (rank‘𝑧) = (rank‘{𝑥}))
8863, 87abrexco 6661 . . . . . . . . . . 11 {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
8988unieqi 4593 . . . . . . . . . 10 {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
9086, 89eqtri 2778 . . . . . . . . 9 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧) = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
9184, 90syl6req 2807 . . . . . . . 8 (𝐴 (𝑅1 “ On) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴))
9247, 91syl 17 . . . . . . 7 (Lim (rank‘𝐴) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴))
93 fvex 6358 . . . . . . . 8 (rank‘𝐴) ∈ V
9493cfslb 9276 . . . . . . 7 ((Lim (rank‘𝐴) ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴) ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴)) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
9562, 92, 94mpd3an23 1571 . . . . . 6 (Lim (rank‘𝐴) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
96 fveq2 6348 . . . . . . . . . . 11 (𝑦 = 𝐴 → (rank‘𝑦) = (rank‘𝐴))
9796fveq2d 6352 . . . . . . . . . 10 (𝑦 = 𝐴 → (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴)))
98 breq12 4805 . . . . . . . . . 10 ((𝑦 = 𝐴 ∧ (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴))) → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴))))
9997, 98mpdan 705 . . . . . . . . 9 (𝑦 = 𝐴 → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴))))
100 rexeq 3274 . . . . . . . . . . 11 (𝑦 = 𝐴 → (∃𝑥𝑦 𝑤 = (rank‘{𝑥}) ↔ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})))
101100abbidv 2875 . . . . . . . . . 10 (𝑦 = 𝐴 → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
102 breq12 4805 . . . . . . . . . 10 (({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ 𝑦 = 𝐴) → ({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
103101, 102mpancom 706 . . . . . . . . 9 (𝑦 = 𝐴 → ({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
10499, 103imbi12d 333 . . . . . . . 8 (𝑦 = 𝐴 → ((𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦) ↔ (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴)))
105 eqid 2756 . . . . . . . . . 10 (𝑥𝑦 ↦ (rank‘{𝑥})) = (𝑥𝑦 ↦ (rank‘{𝑥}))
106105rnmpt 5522 . . . . . . . . 9 ran (𝑥𝑦 ↦ (rank‘{𝑥})) = {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})}
107 cfon 9265 . . . . . . . . . . 11 (cf‘(rank‘𝑦)) ∈ On
108 sdomdom 8145 . . . . . . . . . . 11 (𝑦 ≺ (cf‘(rank‘𝑦)) → 𝑦 ≼ (cf‘(rank‘𝑦)))
109 ondomen 9046 . . . . . . . . . . 11 (((cf‘(rank‘𝑦)) ∈ On ∧ 𝑦 ≼ (cf‘(rank‘𝑦))) → 𝑦 ∈ dom card)
110107, 108, 109sylancr 698 . . . . . . . . . 10 (𝑦 ≺ (cf‘(rank‘𝑦)) → 𝑦 ∈ dom card)
111 fvex 6358 . . . . . . . . . . . 12 (rank‘{𝑥}) ∈ V
112111, 105fnmpti 6179 . . . . . . . . . . 11 (𝑥𝑦 ↦ (rank‘{𝑥})) Fn 𝑦
113 dffn4 6278 . . . . . . . . . . 11 ((𝑥𝑦 ↦ (rank‘{𝑥})) Fn 𝑦 ↔ (𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥})))
114112, 113mpbi 220 . . . . . . . . . 10 (𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥}))
115 fodomnum 9066 . . . . . . . . . 10 (𝑦 ∈ dom card → ((𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥})) → ran (𝑥𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦))
116110, 114, 115mpisyl 21 . . . . . . . . 9 (𝑦 ≺ (cf‘(rank‘𝑦)) → ran (𝑥𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦)
117106, 116syl5eqbrr 4836 . . . . . . . 8 (𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦)
118104, 117vtoclg 3402 . . . . . . 7 (𝐴 (𝑅1 “ On) → (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
11947, 118syl 17 . . . . . 6 (Lim (rank‘𝐴) → (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
120 domtr 8170 . . . . . . 7 (((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → (cf‘(rank‘𝐴)) ≼ 𝐴)
121120, 41syl 17 . . . . . 6 (((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
12295, 119, 121syl6an 569 . . . . 5 (Lim (rank‘𝐴) → (𝐴 ≺ (cf‘(rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴))))
123122pm2.01d 181 . . . 4 (Lim (rank‘𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
124123adantl 473 . . 3 (((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
1259, 42, 1243jaoi 1536 . 2 (((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴))) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
1263, 125ax-mp 5 1 ¬ 𝐴 ≺ (cf‘(rank‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3o 1071   = wceq 1628  wcel 2135  {cab 2742  wne 2928  wrex 3047  Vcvv 3336  wss 3711  c0 4054  {csn 4317   cuni 4584   ciun 4668   class class class wbr 4800  cmpt 4877  dom cdm 5262  ran crn 5263  cima 5265  Oncon0 5880  Lim wlim 5881  suc csuc 5882   Fn wfn 6040  ontowfo 6043  cfv 6045  1𝑜c1o 7718  cdom 8115  csdm 8116  𝑅1cr1 8794  rankcrnk 8795  cardccrd 8947  cfccf 8949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-iin 4671  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-se 5222  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-isom 6054  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-1o 7725  df-er 7907  df-map 8021  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-r1 8796  df-rank 8797  df-card 8951  df-cf 8953  df-acn 8954
This theorem is referenced by:  inatsk  9788  grur1  9830
  Copyright terms: Public domain W3C validator