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

Theorem rankcf 9914
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 8935 . . 3 (rank‘𝐴) ∈ On
2 onzsl 7307 . . 3 ((rank‘𝐴) ∈ On ↔ ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴))))
31, 2mpbi 222 . 2 ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)))
4 sdom0 8361 . . . 4 ¬ 𝐴 ≺ ∅
5 fveq2 6433 . . . . . 6 ((rank‘𝐴) = ∅ → (cf‘(rank‘𝐴)) = (cf‘∅))
6 cf0 9388 . . . . . 6 (cf‘∅) = ∅
75, 6syl6eq 2877 . . . . 5 ((rank‘𝐴) = ∅ → (cf‘(rank‘𝐴)) = ∅)
87breq2d 4885 . . . 4 ((rank‘𝐴) = ∅ → (𝐴 ≺ (cf‘(rank‘𝐴)) ↔ 𝐴 ≺ ∅))
94, 8mtbiri 319 . . 3 ((rank‘𝐴) = ∅ → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
10 fveq2 6433 . . . . . . 7 ((rank‘𝐴) = suc 𝑥 → (cf‘(rank‘𝐴)) = (cf‘suc 𝑥))
11 cfsuc 9394 . . . . . . 7 (𝑥 ∈ On → (cf‘suc 𝑥) = 1o)
1210, 11sylan9eqr 2883 . . . . . 6 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → (cf‘(rank‘𝐴)) = 1o)
13 nsuceq0 6043 . . . . . . . . 9 suc 𝑥 ≠ ∅
14 neeq1 3061 . . . . . . . . 9 ((rank‘𝐴) = suc 𝑥 → ((rank‘𝐴) ≠ ∅ ↔ suc 𝑥 ≠ ∅))
1513, 14mpbiri 250 . . . . . . . 8 ((rank‘𝐴) = suc 𝑥 → (rank‘𝐴) ≠ ∅)
16 fveq2 6433 . . . . . . . . . . 11 (𝐴 = ∅ → (rank‘𝐴) = (rank‘∅))
17 0elon 6016 . . . . . . . . . . . . 13 ∅ ∈ On
18 r1fnon 8907 . . . . . . . . . . . . . 14 𝑅1 Fn On
19 fndm 6223 . . . . . . . . . . . . . 14 (𝑅1 Fn On → dom 𝑅1 = On)
2018, 19ax-mp 5 . . . . . . . . . . . . 13 dom 𝑅1 = On
2117, 20eleqtrri 2905 . . . . . . . . . . . 12 ∅ ∈ dom 𝑅1
22 rankonid 8969 . . . . . . . . . . . 12 (∅ ∈ dom 𝑅1 ↔ (rank‘∅) = ∅)
2321, 22mpbi 222 . . . . . . . . . . 11 (rank‘∅) = ∅
2416, 23syl6eq 2877 . . . . . . . . . 10 (𝐴 = ∅ → (rank‘𝐴) = ∅)
2524necon3i 3031 . . . . . . . . 9 ((rank‘𝐴) ≠ ∅ → 𝐴 ≠ ∅)
26 rankvaln 8939 . . . . . . . . . . 11 𝐴 (𝑅1 “ On) → (rank‘𝐴) = ∅)
2726necon1ai 3026 . . . . . . . . . 10 ((rank‘𝐴) ≠ ∅ → 𝐴 (𝑅1 “ On))
28 breq2 4877 . . . . . . . . . . 11 (𝑦 = 𝐴 → (1o𝑦 ↔ 1o𝐴))
29 neeq1 3061 . . . . . . . . . . 11 (𝑦 = 𝐴 → (𝑦 ≠ ∅ ↔ 𝐴 ≠ ∅))
30 0sdom1dom 8427 . . . . . . . . . . . 12 (∅ ≺ 𝑦 ↔ 1o𝑦)
31 vex 3417 . . . . . . . . . . . . 13 𝑦 ∈ V
32310sdom 8360 . . . . . . . . . . . 12 (∅ ≺ 𝑦𝑦 ≠ ∅)
3330, 32bitr3i 269 . . . . . . . . . . 11 (1o𝑦𝑦 ≠ ∅)
3428, 29, 33vtoclbg 3483 . . . . . . . . . 10 (𝐴 (𝑅1 “ On) → (1o𝐴𝐴 ≠ ∅))
3527, 34syl 17 . . . . . . . . 9 ((rank‘𝐴) ≠ ∅ → (1o𝐴𝐴 ≠ ∅))
3625, 35mpbird 249 . . . . . . . 8 ((rank‘𝐴) ≠ ∅ → 1o𝐴)
3715, 36syl 17 . . . . . . 7 ((rank‘𝐴) = suc 𝑥 → 1o𝐴)
3837adantl 475 . . . . . 6 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → 1o𝐴)
3912, 38eqbrtrd 4895 . . . . 5 ((𝑥 ∈ On ∧ (rank‘𝐴) = suc 𝑥) → (cf‘(rank‘𝐴)) ≼ 𝐴)
4039rexlimiva 3237 . . . 4 (∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 → (cf‘(rank‘𝐴)) ≼ 𝐴)
41 domnsym 8355 . . . 4 ((cf‘(rank‘𝐴)) ≼ 𝐴 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
4240, 41syl 17 . . 3 (∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
43 nlim0 6021 . . . . . . . . . . . . . . . . 17 ¬ Lim ∅
44 limeq 5975 . . . . . . . . . . . . . . . . 17 ((rank‘𝐴) = ∅ → (Lim (rank‘𝐴) ↔ Lim ∅))
4543, 44mtbiri 319 . . . . . . . . . . . . . . . 16 ((rank‘𝐴) = ∅ → ¬ Lim (rank‘𝐴))
4626, 45syl 17 . . . . . . . . . . . . . . 15 𝐴 (𝑅1 “ On) → ¬ Lim (rank‘𝐴))
4746con4i 114 . . . . . . . . . . . . . 14 (Lim (rank‘𝐴) → 𝐴 (𝑅1 “ On))
48 r1elssi 8945 . . . . . . . . . . . . . 14 (𝐴 (𝑅1 “ On) → 𝐴 (𝑅1 “ On))
4947, 48syl 17 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → 𝐴 (𝑅1 “ On))
5049sselda 3827 . . . . . . . . . . . 12 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → 𝑥 (𝑅1 “ On))
51 ranksnb 8967 . . . . . . . . . . . 12 (𝑥 (𝑅1 “ On) → (rank‘{𝑥}) = suc (rank‘𝑥))
5250, 51syl 17 . . . . . . . . . . 11 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (rank‘{𝑥}) = suc (rank‘𝑥))
53 rankelb 8964 . . . . . . . . . . . . . 14 (𝐴 (𝑅1 “ On) → (𝑥𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
5447, 53syl 17 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → (𝑥𝐴 → (rank‘𝑥) ∈ (rank‘𝐴)))
55 limsuc 7310 . . . . . . . . . . . . 13 (Lim (rank‘𝐴) → ((rank‘𝑥) ∈ (rank‘𝐴) ↔ suc (rank‘𝑥) ∈ (rank‘𝐴)))
5654, 55sylibd 231 . . . . . . . . . . . 12 (Lim (rank‘𝐴) → (𝑥𝐴 → suc (rank‘𝑥) ∈ (rank‘𝐴)))
5756imp 397 . . . . . . . . . . 11 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → suc (rank‘𝑥) ∈ (rank‘𝐴))
5852, 57eqeltrd 2906 . . . . . . . . . 10 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (rank‘{𝑥}) ∈ (rank‘𝐴))
59 eleq1a 2901 . . . . . . . . . 10 ((rank‘{𝑥}) ∈ (rank‘𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6058, 59syl 17 . . . . . . . . 9 ((Lim (rank‘𝐴) ∧ 𝑥𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6160rexlimdva 3240 . . . . . . . 8 (Lim (rank‘𝐴) → (∃𝑥𝐴 𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴)))
6261abssdv 3901 . . . . . . 7 (Lim (rank‘𝐴) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴))
63 snex 5129 . . . . . . . . . . . . 13 {𝑥} ∈ V
6463dfiun2 4774 . . . . . . . . . . . 12 𝑥𝐴 {𝑥} = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}
65 iunid 4795 . . . . . . . . . . . 12 𝑥𝐴 {𝑥} = 𝐴
6664, 65eqtr3i 2851 . . . . . . . . . . 11 {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} = 𝐴
6766fveq2i 6436 . . . . . . . . . 10 (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = (rank‘𝐴)
6848sselda 3827 . . . . . . . . . . . . . . 15 ((𝐴 (𝑅1 “ On) ∧ 𝑥𝐴) → 𝑥 (𝑅1 “ On))
69 snwf 8949 . . . . . . . . . . . . . . 15 (𝑥 (𝑅1 “ On) → {𝑥} ∈ (𝑅1 “ On))
70 eleq1a 2901 . . . . . . . . . . . . . . 15 ({𝑥} ∈ (𝑅1 “ On) → (𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7168, 69, 703syl 18 . . . . . . . . . . . . . 14 ((𝐴 (𝑅1 “ On) ∧ 𝑥𝐴) → (𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7271rexlimdva 3240 . . . . . . . . . . . . 13 (𝐴 (𝑅1 “ On) → (∃𝑥𝐴 𝑦 = {𝑥} → 𝑦 (𝑅1 “ On)))
7372abssdv 3901 . . . . . . . . . . . 12 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On))
74 abrexexg 7402 . . . . . . . . . . . . 13 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ V)
75 eleq1 2894 . . . . . . . . . . . . . 14 (𝑧 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} → (𝑧 (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On)))
76 sseq1 3851 . . . . . . . . . . . . . 14 (𝑧 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} → (𝑧 (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
77 vex 3417 . . . . . . . . . . . . . . 15 𝑧 ∈ V
7877r1elss 8946 . . . . . . . . . . . . . 14 (𝑧 (𝑅1 “ On) ↔ 𝑧 (𝑅1 “ On))
7975, 76, 78vtoclbg 3483 . . . . . . . . . . . . 13 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ V → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
8074, 79syl 17 . . . . . . . . . . . 12 (𝐴 (𝑅1 “ On) → ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ⊆ (𝑅1 “ On)))
8173, 80mpbird 249 . . . . . . . . . . 11 (𝐴 (𝑅1 “ On) → {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On))
82 rankuni2b 8993 . . . . . . . . . . 11 ({𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} ∈ (𝑅1 “ On) → (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
8381, 82syl 17 . . . . . . . . . 10 (𝐴 (𝑅1 “ On) → (rank‘ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
8467, 83syl5eqr 2875 . . . . . . . . 9 (𝐴 (𝑅1 “ On) → (rank‘𝐴) = 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧))
85 fvex 6446 . . . . . . . . . . 11 (rank‘𝑧) ∈ V
8685dfiun2 4774 . . . . . . . . . 10 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧) = {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)}
87 fveq2 6433 . . . . . . . . . . . 12 (𝑧 = {𝑥} → (rank‘𝑧) = (rank‘{𝑥}))
8863, 87abrexco 6757 . . . . . . . . . . 11 {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
8988unieqi 4667 . . . . . . . . . 10 {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
9086, 89eqtri 2849 . . . . . . . . 9 𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = {𝑥}} (rank‘𝑧) = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})}
9184, 90syl6req 2878 . . . . . . . 8 (𝐴 (𝑅1 “ On) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴))
9247, 91syl 17 . . . . . . 7 (Lim (rank‘𝐴) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴))
93 fvex 6446 . . . . . . . 8 (rank‘𝐴) ∈ V
9493cfslb 9403 . . . . . . 7 ((Lim (rank‘𝐴) ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴) ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴)) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
9562, 92, 94mpd3an23 1593 . . . . . 6 (Lim (rank‘𝐴) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
96 2fveq3 6438 . . . . . . . . . 10 (𝑦 = 𝐴 → (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴)))
97 breq12 4878 . . . . . . . . . 10 ((𝑦 = 𝐴 ∧ (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴))) → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴))))
9896, 97mpdan 680 . . . . . . . . 9 (𝑦 = 𝐴 → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴))))
99 rexeq 3351 . . . . . . . . . . 11 (𝑦 = 𝐴 → (∃𝑥𝑦 𝑤 = (rank‘{𝑥}) ↔ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})))
10099abbidv 2946 . . . . . . . . . 10 (𝑦 = 𝐴 → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})})
101 breq12 4878 . . . . . . . . . 10 (({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ 𝑦 = 𝐴) → ({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
102100, 101mpancom 681 . . . . . . . . 9 (𝑦 = 𝐴 → ({𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
10398, 102imbi12d 336 . . . . . . . 8 (𝑦 = 𝐴 → ((𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦) ↔ (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴)))
104 eqid 2825 . . . . . . . . . 10 (𝑥𝑦 ↦ (rank‘{𝑥})) = (𝑥𝑦 ↦ (rank‘{𝑥}))
105104rnmpt 5604 . . . . . . . . 9 ran (𝑥𝑦 ↦ (rank‘{𝑥})) = {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})}
106 cfon 9392 . . . . . . . . . . 11 (cf‘(rank‘𝑦)) ∈ On
107 sdomdom 8250 . . . . . . . . . . 11 (𝑦 ≺ (cf‘(rank‘𝑦)) → 𝑦 ≼ (cf‘(rank‘𝑦)))
108 ondomen 9173 . . . . . . . . . . 11 (((cf‘(rank‘𝑦)) ∈ On ∧ 𝑦 ≼ (cf‘(rank‘𝑦))) → 𝑦 ∈ dom card)
109106, 107, 108sylancr 583 . . . . . . . . . 10 (𝑦 ≺ (cf‘(rank‘𝑦)) → 𝑦 ∈ dom card)
110 fvex 6446 . . . . . . . . . . . 12 (rank‘{𝑥}) ∈ V
111110, 104fnmpti 6255 . . . . . . . . . . 11 (𝑥𝑦 ↦ (rank‘{𝑥})) Fn 𝑦
112 dffn4 6359 . . . . . . . . . . 11 ((𝑥𝑦 ↦ (rank‘{𝑥})) Fn 𝑦 ↔ (𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥})))
113111, 112mpbi 222 . . . . . . . . . 10 (𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥}))
114 fodomnum 9193 . . . . . . . . . 10 (𝑦 ∈ dom card → ((𝑥𝑦 ↦ (rank‘{𝑥})):𝑦onto→ran (𝑥𝑦 ↦ (rank‘{𝑥})) → ran (𝑥𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦))
115109, 113, 114mpisyl 21 . . . . . . . . 9 (𝑦 ≺ (cf‘(rank‘𝑦)) → ran (𝑥𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦)
116105, 115syl5eqbrr 4909 . . . . . . . 8 (𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦)
117103, 116vtoclg 3482 . . . . . . 7 (𝐴 (𝑅1 “ On) → (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
11847, 117syl 17 . . . . . 6 (Lim (rank‘𝐴) → (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))
119 domtr 8275 . . . . . . 7 (((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → (cf‘(rank‘𝐴)) ≼ 𝐴)
120119, 41syl 17 . . . . . 6 (((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
12195, 118, 120syl6an 676 . . . . 5 (Lim (rank‘𝐴) → (𝐴 ≺ (cf‘(rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴))))
122121pm2.01d 182 . . . 4 (Lim (rank‘𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
123122adantl 475 . . 3 (((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴)))
1249, 42, 1233jaoi 1558 . 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 198  wa 386  w3o 1112   = wceq 1658  wcel 2166  {cab 2811  wne 2999  wrex 3118  Vcvv 3414  wss 3798  c0 4144  {csn 4397   cuni 4658   ciun 4740   class class class wbr 4873  cmpt 4952  dom cdm 5342  ran crn 5343  cima 5345  Oncon0 5963  Lim wlim 5964  suc csuc 5965   Fn wfn 6118  ontowfo 6121  cfv 6123  1oc1o 7819  cdom 8220  csdm 8221  𝑅1cr1 8902  rankcrnk 8903  cardccrd 9074  cfccf 9076
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-iin 4743  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-er 8009  df-map 8124  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-r1 8904  df-rank 8905  df-card 9078  df-cf 9080  df-acn 9081
This theorem is referenced by:  inatsk  9915  grur1  9957
  Copyright terms: Public domain W3C validator