| Step | Hyp | Ref
| Expression |
| 1 | | rankon 9835 |
. . 3
⊢
(rank‘𝐴)
∈ On |
| 2 | | onzsl 7867 |
. . 3
⊢
((rank‘𝐴)
∈ On ↔ ((rank‘𝐴) = ∅ ∨ ∃𝑥 ∈ On (rank‘𝐴) = suc 𝑥 ∨ ((rank‘𝐴) ∈ V ∧ Lim (rank‘𝐴)))) |
| 3 | 1, 2 | mpbi 230 |
. 2
⊢
((rank‘𝐴) =
∅ ∨ ∃𝑥
∈ On (rank‘𝐴) =
suc 𝑥 ∨
((rank‘𝐴) ∈ V
∧ Lim (rank‘𝐴))) |
| 4 | | sdom0 9148 |
. . . 4
⊢ ¬
𝐴 ≺
∅ |
| 5 | | fveq2 6906 |
. . . . . 6
⊢
((rank‘𝐴) =
∅ → (cf‘(rank‘𝐴)) = (cf‘∅)) |
| 6 | | cf0 10291 |
. . . . . 6
⊢
(cf‘∅) = ∅ |
| 7 | 5, 6 | eqtrdi 2793 |
. . . . 5
⊢
((rank‘𝐴) =
∅ → (cf‘(rank‘𝐴)) = ∅) |
| 8 | 7 | breq2d 5155 |
. . . 4
⊢
((rank‘𝐴) =
∅ → (𝐴 ≺
(cf‘(rank‘𝐴))
↔ 𝐴 ≺
∅)) |
| 9 | 4, 8 | mtbiri 327 |
. . 3
⊢
((rank‘𝐴) =
∅ → ¬ 𝐴
≺ (cf‘(rank‘𝐴))) |
| 10 | | fveq2 6906 |
. . . . . . 7
⊢
((rank‘𝐴) =
suc 𝑥 →
(cf‘(rank‘𝐴)) =
(cf‘suc 𝑥)) |
| 11 | | cfsuc 10297 |
. . . . . . 7
⊢ (𝑥 ∈ On → (cf‘suc
𝑥) =
1o) |
| 12 | 10, 11 | sylan9eqr 2799 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧
(rank‘𝐴) = suc 𝑥) →
(cf‘(rank‘𝐴)) =
1o) |
| 13 | | nsuceq0 6467 |
. . . . . . . . 9
⊢ suc 𝑥 ≠ ∅ |
| 14 | | neeq1 3003 |
. . . . . . . . 9
⊢
((rank‘𝐴) =
suc 𝑥 →
((rank‘𝐴) ≠
∅ ↔ suc 𝑥 ≠
∅)) |
| 15 | 13, 14 | mpbiri 258 |
. . . . . . . 8
⊢
((rank‘𝐴) =
suc 𝑥 →
(rank‘𝐴) ≠
∅) |
| 16 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ →
(rank‘𝐴) =
(rank‘∅)) |
| 17 | | 0elon 6438 |
. . . . . . . . . . . . 13
⊢ ∅
∈ On |
| 18 | | r1fnon 9807 |
. . . . . . . . . . . . . 14
⊢
𝑅1 Fn On |
| 19 | 18 | fndmi 6672 |
. . . . . . . . . . . . 13
⊢ dom
𝑅1 = On |
| 20 | 17, 19 | eleqtrri 2840 |
. . . . . . . . . . . 12
⊢ ∅
∈ dom 𝑅1 |
| 21 | | rankonid 9869 |
. . . . . . . . . . . 12
⊢ (∅
∈ dom 𝑅1 ↔ (rank‘∅) =
∅) |
| 22 | 20, 21 | mpbi 230 |
. . . . . . . . . . 11
⊢
(rank‘∅) = ∅ |
| 23 | 16, 22 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ →
(rank‘𝐴) =
∅) |
| 24 | 23 | necon3i 2973 |
. . . . . . . . 9
⊢
((rank‘𝐴) ≠
∅ → 𝐴 ≠
∅) |
| 25 | | rankvaln 9839 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) =
∅) |
| 26 | 25 | necon1ai 2968 |
. . . . . . . . . 10
⊢
((rank‘𝐴) ≠
∅ → 𝐴 ∈
∪ (𝑅1 “
On)) |
| 27 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (1o ≼ 𝑦 ↔ 1o ≼
𝐴)) |
| 28 | | neeq1 3003 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (𝑦 ≠ ∅ ↔ 𝐴 ≠ ∅)) |
| 29 | | 0sdom1dom 9274 |
. . . . . . . . . . . 12
⊢ (∅
≺ 𝑦 ↔
1o ≼ 𝑦) |
| 30 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
| 31 | 30 | 0sdom 9147 |
. . . . . . . . . . . 12
⊢ (∅
≺ 𝑦 ↔ 𝑦 ≠ ∅) |
| 32 | 29, 31 | bitr3i 277 |
. . . . . . . . . . 11
⊢
(1o ≼ 𝑦 ↔ 𝑦 ≠ ∅) |
| 33 | 27, 28, 32 | vtoclbg 3557 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (1o
≼ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 34 | 26, 33 | syl 17 |
. . . . . . . . 9
⊢
((rank‘𝐴) ≠
∅ → (1o ≼ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 35 | 24, 34 | mpbird 257 |
. . . . . . . 8
⊢
((rank‘𝐴) ≠
∅ → 1o ≼ 𝐴) |
| 36 | 15, 35 | syl 17 |
. . . . . . 7
⊢
((rank‘𝐴) =
suc 𝑥 → 1o
≼ 𝐴) |
| 37 | 36 | adantl 481 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧
(rank‘𝐴) = suc 𝑥) → 1o ≼
𝐴) |
| 38 | 12, 37 | eqbrtrd 5165 |
. . . . 5
⊢ ((𝑥 ∈ On ∧
(rank‘𝐴) = suc 𝑥) →
(cf‘(rank‘𝐴))
≼ 𝐴) |
| 39 | 38 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑥 ∈ On
(rank‘𝐴) = suc 𝑥 →
(cf‘(rank‘𝐴))
≼ 𝐴) |
| 40 | | domnsym 9139 |
. . . 4
⊢
((cf‘(rank‘𝐴)) ≼ 𝐴 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴))) |
| 41 | 39, 40 | syl 17 |
. . 3
⊢
(∃𝑥 ∈ On
(rank‘𝐴) = suc 𝑥 → ¬ 𝐴 ≺ (cf‘(rank‘𝐴))) |
| 42 | | nlim0 6443 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
Lim ∅ |
| 43 | | limeq 6396 |
. . . . . . . . . . . . . . . . 17
⊢
((rank‘𝐴) =
∅ → (Lim (rank‘𝐴) ↔ Lim ∅)) |
| 44 | 42, 43 | mtbiri 327 |
. . . . . . . . . . . . . . . 16
⊢
((rank‘𝐴) =
∅ → ¬ Lim (rank‘𝐴)) |
| 45 | 25, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝐴 ∈ ∪ (𝑅1 “ On) → ¬ Lim
(rank‘𝐴)) |
| 46 | 45 | con4i 114 |
. . . . . . . . . . . . . 14
⊢ (Lim
(rank‘𝐴) → 𝐴 ∈ ∪ (𝑅1 “ On)) |
| 47 | | r1elssi 9845 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On)) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ (Lim
(rank‘𝐴) → 𝐴 ⊆ ∪ (𝑅1 “ On)) |
| 49 | 48 | sselda 3983 |
. . . . . . . . . . . 12
⊢ ((Lim
(rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
| 50 | | ranksnb 9867 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) →
(rank‘{𝑥}) = suc
(rank‘𝑥)) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
⊢ ((Lim
(rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → (rank‘{𝑥}) = suc (rank‘𝑥)) |
| 52 | | rankelb 9864 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴))) |
| 53 | 46, 52 | syl 17 |
. . . . . . . . . . . . 13
⊢ (Lim
(rank‘𝐴) →
(𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴))) |
| 54 | | limsuc 7870 |
. . . . . . . . . . . . 13
⊢ (Lim
(rank‘𝐴) →
((rank‘𝑥) ∈
(rank‘𝐴) ↔ suc
(rank‘𝑥) ∈
(rank‘𝐴))) |
| 55 | 53, 54 | sylibd 239 |
. . . . . . . . . . . 12
⊢ (Lim
(rank‘𝐴) →
(𝑥 ∈ 𝐴 → suc (rank‘𝑥) ∈ (rank‘𝐴))) |
| 56 | 55 | imp 406 |
. . . . . . . . . . 11
⊢ ((Lim
(rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → suc (rank‘𝑥) ∈ (rank‘𝐴)) |
| 57 | 51, 56 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ ((Lim
(rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → (rank‘{𝑥}) ∈ (rank‘𝐴)) |
| 58 | | eleq1a 2836 |
. . . . . . . . . 10
⊢
((rank‘{𝑥})
∈ (rank‘𝐴)
→ (𝑤 =
(rank‘{𝑥}) →
𝑤 ∈ (rank‘𝐴))) |
| 59 | 57, 58 | syl 17 |
. . . . . . . . 9
⊢ ((Lim
(rank‘𝐴) ∧ 𝑥 ∈ 𝐴) → (𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴))) |
| 60 | 59 | rexlimdva 3155 |
. . . . . . . 8
⊢ (Lim
(rank‘𝐴) →
(∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥}) → 𝑤 ∈ (rank‘𝐴))) |
| 61 | 60 | abssdv 4068 |
. . . . . . 7
⊢ (Lim
(rank‘𝐴) →
{𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴)) |
| 62 | | vsnex 5434 |
. . . . . . . . . . . . 13
⊢ {𝑥} ∈ V |
| 63 | 62 | dfiun2 5033 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = ∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} |
| 64 | | iunid 5060 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
| 65 | 63, 64 | eqtr3i 2767 |
. . . . . . . . . . 11
⊢ ∪ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = {𝑥}} = 𝐴 |
| 66 | 65 | fveq2i 6909 |
. . . . . . . . . 10
⊢
(rank‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}) = (rank‘𝐴) |
| 67 | 47 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ∪
(𝑅1 “ On)) |
| 68 | | snwf 9849 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ∪ (𝑅1 “ On) → {𝑥} ∈ ∪ (𝑅1 “ On)) |
| 69 | | eleq1a 2836 |
. . . . . . . . . . . . . . 15
⊢ ({𝑥} ∈ ∪ (𝑅1 “ On) → (𝑦 = {𝑥} → 𝑦 ∈ ∪
(𝑅1 “ On))) |
| 70 | 67, 68, 69 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ 𝐴) → (𝑦 = {𝑥} → 𝑦 ∈ ∪
(𝑅1 “ On))) |
| 71 | 70 | rexlimdva 3155 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (∃𝑥 ∈ 𝐴 𝑦 = {𝑥} → 𝑦 ∈ ∪
(𝑅1 “ On))) |
| 72 | 71 | abssdv 4068 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ⊆ ∪
(𝑅1 “ On)) |
| 73 | | abrexexg 7985 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ V) |
| 74 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} → (𝑧 ∈ ∪
(𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪
(𝑅1 “ On))) |
| 75 | | sseq1 4009 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} → (𝑧 ⊆ ∪
(𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ⊆ ∪
(𝑅1 “ On))) |
| 76 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
| 77 | 76 | r1elss 9846 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ∪ (𝑅1 “ On) ↔ 𝑧 ⊆ ∪ (𝑅1 “ On)) |
| 78 | 74, 75, 77 | vtoclbg 3557 |
. . . . . . . . . . . . 13
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ V → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪
(𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ⊆ ∪
(𝑅1 “ On))) |
| 79 | 73, 78 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪
(𝑅1 “ On) ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ⊆ ∪
(𝑅1 “ On))) |
| 80 | 72, 79 | mpbird 257 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪
(𝑅1 “ On)) |
| 81 | | rankuni2b 9893 |
. . . . . . . . . . 11
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} ∈ ∪
(𝑅1 “ On) → (rank‘∪ {𝑦
∣ ∃𝑥 ∈
𝐴 𝑦 = {𝑥}}) = ∪
𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧)) |
| 82 | 80, 81 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘∪ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}) = ∪
𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧)) |
| 83 | 66, 82 | eqtr3id 2791 |
. . . . . . . . 9
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) = ∪ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧)) |
| 84 | | fvex 6919 |
. . . . . . . . . . 11
⊢
(rank‘𝑧)
∈ V |
| 85 | 84 | dfiun2 5033 |
. . . . . . . . . 10
⊢ ∪ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧) = ∪ {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} |
| 86 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑧 = {𝑥} → (rank‘𝑧) = (rank‘{𝑥})) |
| 87 | 62, 86 | abrexco 7264 |
. . . . . . . . . . 11
⊢ {𝑤 ∣ ∃𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} |
| 88 | 87 | unieqi 4919 |
. . . . . . . . . 10
⊢ ∪ {𝑤
∣ ∃𝑧 ∈
{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}}𝑤 = (rank‘𝑧)} = ∪ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} |
| 89 | 85, 88 | eqtri 2765 |
. . . . . . . . 9
⊢ ∪ 𝑧 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = {𝑥}} (rank‘𝑧) = ∪ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} |
| 90 | 83, 89 | eqtr2di 2794 |
. . . . . . . 8
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∪ {𝑤
∣ ∃𝑥 ∈
𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴)) |
| 91 | 46, 90 | syl 17 |
. . . . . . 7
⊢ (Lim
(rank‘𝐴) → ∪ {𝑤
∣ ∃𝑥 ∈
𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴)) |
| 92 | | fvex 6919 |
. . . . . . . 8
⊢
(rank‘𝐴)
∈ V |
| 93 | 92 | cfslb 10306 |
. . . . . . 7
⊢ ((Lim
(rank‘𝐴) ∧ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ⊆ (rank‘𝐴) ∧ ∪ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} = (rank‘𝐴)) → (cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})}) |
| 94 | 61, 91, 93 | mpd3an23 1465 |
. . . . . 6
⊢ (Lim
(rank‘𝐴) →
(cf‘(rank‘𝐴))
≼ {𝑤 ∣
∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})}) |
| 95 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴))) |
| 96 | | breq12 5148 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝐴 ∧ (cf‘(rank‘𝑦)) = (cf‘(rank‘𝐴))) → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴)))) |
| 97 | 95, 96 | mpdan 687 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝑦 ≺ (cf‘(rank‘𝑦)) ↔ 𝐴 ≺ (cf‘(rank‘𝐴)))) |
| 98 | | rexeq 3322 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥}) ↔ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥}))) |
| 99 | 98 | abbidv 2808 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → {𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})}) |
| 100 | | breq12 5148 |
. . . . . . . . . 10
⊢ (({𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} = {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ∧ 𝑦 = 𝐴) → ({𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴)) |
| 101 | 99, 100 | mpancom 688 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ({𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦 ↔ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴)) |
| 102 | 97, 101 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → ((𝑦 ≺ (cf‘(rank‘𝑦)) → {𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦) ↔ (𝐴 ≺ (cf‘(rank‘𝐴)) → {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴))) |
| 103 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) = (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) |
| 104 | 103 | rnmpt 5968 |
. . . . . . . . 9
⊢ ran
(𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) = {𝑤 ∣ ∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} |
| 105 | | cfon 10295 |
. . . . . . . . . . 11
⊢
(cf‘(rank‘𝑦)) ∈ On |
| 106 | | sdomdom 9020 |
. . . . . . . . . . 11
⊢ (𝑦 ≺
(cf‘(rank‘𝑦))
→ 𝑦 ≼
(cf‘(rank‘𝑦))) |
| 107 | | ondomen 10077 |
. . . . . . . . . . 11
⊢
(((cf‘(rank‘𝑦)) ∈ On ∧ 𝑦 ≼ (cf‘(rank‘𝑦))) → 𝑦 ∈ dom card) |
| 108 | 105, 106,
107 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝑦 ≺
(cf‘(rank‘𝑦))
→ 𝑦 ∈ dom
card) |
| 109 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(rank‘{𝑥})
∈ V |
| 110 | 109, 103 | fnmpti 6711 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) Fn 𝑦 |
| 111 | | dffn4 6826 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) Fn 𝑦 ↔ (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})):𝑦–onto→ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥}))) |
| 112 | 110, 111 | mpbi 230 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})):𝑦–onto→ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) |
| 113 | | fodomnum 10097 |
. . . . . . . . . 10
⊢ (𝑦 ∈ dom card → ((𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})):𝑦–onto→ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) → ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦)) |
| 114 | 108, 112,
113 | mpisyl 21 |
. . . . . . . . 9
⊢ (𝑦 ≺
(cf‘(rank‘𝑦))
→ ran (𝑥 ∈ 𝑦 ↦ (rank‘{𝑥})) ≼ 𝑦) |
| 115 | 104, 114 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ (𝑦 ≺
(cf‘(rank‘𝑦))
→ {𝑤 ∣
∃𝑥 ∈ 𝑦 𝑤 = (rank‘{𝑥})} ≼ 𝑦) |
| 116 | 102, 115 | vtoclg 3554 |
. . . . . . 7
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝐴 ≺
(cf‘(rank‘𝐴))
→ {𝑤 ∣
∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴)) |
| 117 | 46, 116 | syl 17 |
. . . . . 6
⊢ (Lim
(rank‘𝐴) →
(𝐴 ≺
(cf‘(rank‘𝐴))
→ {𝑤 ∣
∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴)) |
| 118 | | domtr 9047 |
. . . . . . 7
⊢
(((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → (cf‘(rank‘𝐴)) ≼ 𝐴) |
| 119 | 118, 40 | syl 17 |
. . . . . 6
⊢
(((cf‘(rank‘𝐴)) ≼ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ∧ {𝑤 ∣ ∃𝑥 ∈ 𝐴 𝑤 = (rank‘{𝑥})} ≼ 𝐴) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴))) |
| 120 | 94, 117, 119 | syl6an 684 |
. . . . 5
⊢ (Lim
(rank‘𝐴) →
(𝐴 ≺
(cf‘(rank‘𝐴))
→ ¬ 𝐴 ≺
(cf‘(rank‘𝐴)))) |
| 121 | 120 | pm2.01d 190 |
. . . 4
⊢ (Lim
(rank‘𝐴) → ¬
𝐴 ≺
(cf‘(rank‘𝐴))) |
| 122 | 121 | adantl 481 |
. . 3
⊢
(((rank‘𝐴)
∈ V ∧ Lim (rank‘𝐴)) → ¬ 𝐴 ≺ (cf‘(rank‘𝐴))) |
| 123 | 9, 41, 122 | 3jaoi 1430 |
. 2
⊢
(((rank‘𝐴) =
∅ ∨ ∃𝑥
∈ On (rank‘𝐴) =
suc 𝑥 ∨
((rank‘𝐴) ∈ V
∧ Lim (rank‘𝐴)))
→ ¬ 𝐴 ≺
(cf‘(rank‘𝐴))) |
| 124 | 3, 123 | ax-mp 5 |
1
⊢ ¬
𝐴 ≺
(cf‘(rank‘𝐴)) |