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  –onto→wfo 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