Proof of Theorem rankval3b
| Step | Hyp | Ref
| Expression |
| 1 | | rankon 9835 |
. . . . . . . . . 10
⊢
(rank‘𝐴)
∈ On |
| 2 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)) → 𝑥 ∈ On) |
| 3 | | ontri1 6418 |
. . . . . . . . . 10
⊢
(((rank‘𝐴)
∈ On ∧ 𝑥 ∈
On) → ((rank‘𝐴)
⊆ 𝑥 ↔ ¬
𝑥 ∈ (rank‘𝐴))) |
| 4 | 1, 2, 3 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)) → ((rank‘𝐴) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ (rank‘𝐴))) |
| 5 | 4 | con2bid 354 |
. . . . . . . 8
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)) → (𝑥 ∈ (rank‘𝐴) ↔ ¬ (rank‘𝐴) ⊆ 𝑥)) |
| 6 | | r1elssi 9845 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → 𝐴 ⊆ ∪ (𝑅1 “ On)) |
| 7 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ (rank‘𝐴)) → 𝐴 ⊆ ∪
(𝑅1 “ On)) |
| 8 | 7 | sselda 3983 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ (rank‘𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ∪
(𝑅1 “ On)) |
| 9 | | rankdmr1 9841 |
. . . . . . . . . . . . . . . . . 18
⊢
(rank‘𝐴)
∈ dom 𝑅1 |
| 10 | | r1funlim 9806 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Fun
𝑅1 ∧ Lim dom 𝑅1) |
| 11 | 10 | simpri 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ Lim dom
𝑅1 |
| 12 | | limord 6444 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim dom
𝑅1 → Ord dom 𝑅1) |
| 13 | | ordtr1 6427 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord dom
𝑅1 → ((𝑥 ∈ (rank‘𝐴) ∧ (rank‘𝐴) ∈ dom 𝑅1) →
𝑥 ∈ dom
𝑅1)) |
| 14 | 11, 12, 13 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (rank‘𝐴) ∧ (rank‘𝐴) ∈ dom
𝑅1) → 𝑥 ∈ dom
𝑅1) |
| 15 | 9, 14 | mpan2 691 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (rank‘𝐴) → 𝑥 ∈ dom
𝑅1) |
| 16 | 15 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ (rank‘𝐴)) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ dom
𝑅1) |
| 17 | | rankr1ag 9842 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ dom
𝑅1) → (𝑦 ∈ (𝑅1‘𝑥) ↔ (rank‘𝑦) ∈ 𝑥)) |
| 18 | 8, 16, 17 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ (rank‘𝐴)) ∧ 𝑦 ∈ 𝐴) → (𝑦 ∈ (𝑅1‘𝑥) ↔ (rank‘𝑦) ∈ 𝑥)) |
| 19 | 18 | ralbidva 3176 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ (rank‘𝐴)) → (∀𝑦 ∈ 𝐴 𝑦 ∈ (𝑅1‘𝑥) ↔ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)) |
| 20 | 19 | biimpar 477 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ (rank‘𝐴)) ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) → ∀𝑦 ∈ 𝐴 𝑦 ∈ (𝑅1‘𝑥)) |
| 21 | 20 | an32s 652 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) ∧ 𝑥 ∈ (rank‘𝐴)) → ∀𝑦 ∈ 𝐴 𝑦 ∈ (𝑅1‘𝑥)) |
| 22 | | dfss3 3972 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆
(𝑅1‘𝑥) ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ (𝑅1‘𝑥)) |
| 23 | 21, 22 | sylibr 234 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) ∧ 𝑥 ∈ (rank‘𝐴)) → 𝐴 ⊆ (𝑅1‘𝑥)) |
| 24 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) ∧ 𝑥 ∈ (rank‘𝐴)) → 𝐴 ∈ ∪
(𝑅1 “ On)) |
| 25 | 15 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) ∧ 𝑥 ∈ (rank‘𝐴)) → 𝑥 ∈ dom
𝑅1) |
| 26 | | rankr1bg 9843 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝑥 ∈ dom
𝑅1) → (𝐴 ⊆ (𝑅1‘𝑥) ↔ (rank‘𝐴) ⊆ 𝑥)) |
| 27 | 24, 25, 26 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) ∧ 𝑥 ∈ (rank‘𝐴)) → (𝐴 ⊆ (𝑅1‘𝑥) ↔ (rank‘𝐴) ⊆ 𝑥)) |
| 28 | 23, 27 | mpbid 232 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ∪ (𝑅1 “ On) ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) ∧ 𝑥 ∈ (rank‘𝐴)) → (rank‘𝐴) ⊆ 𝑥) |
| 29 | 28 | ex 412 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) → (𝑥 ∈ (rank‘𝐴) → (rank‘𝐴) ⊆ 𝑥)) |
| 30 | 29 | adantrl 716 |
. . . . . . . 8
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)) → (𝑥 ∈ (rank‘𝐴) → (rank‘𝐴) ⊆ 𝑥)) |
| 31 | 5, 30 | sylbird 260 |
. . . . . . 7
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)) → (¬ (rank‘𝐴) ⊆ 𝑥 → (rank‘𝐴) ⊆ 𝑥)) |
| 32 | 31 | pm2.18d 127 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)) → (rank‘𝐴) ⊆ 𝑥) |
| 33 | 32 | ex 412 |
. . . . 5
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) → (rank‘𝐴) ⊆ 𝑥)) |
| 34 | 33 | alrimiv 1927 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∀𝑥((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) → (rank‘𝐴) ⊆ 𝑥)) |
| 35 | | ssintab 4965 |
. . . 4
⊢
((rank‘𝐴)
⊆ ∩ {𝑥 ∣ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)} ↔ ∀𝑥((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥) → (rank‘𝐴) ⊆ 𝑥)) |
| 36 | 34, 35 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) ⊆
∩ {𝑥 ∣ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)}) |
| 37 | | df-rab 3437 |
. . . 4
⊢ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥} = {𝑥 ∣ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)} |
| 38 | 37 | inteqi 4950 |
. . 3
⊢ ∩ {𝑥
∈ On ∣ ∀𝑦
∈ 𝐴 (rank‘𝑦) ∈ 𝑥} = ∩ {𝑥 ∣ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥)} |
| 39 | 36, 38 | sseqtrrdi 4025 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) ⊆
∩ {𝑥 ∈ On ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥}) |
| 40 | | rankelb 9864 |
. . . 4
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑦 ∈ 𝐴 → (rank‘𝑦) ∈ (rank‘𝐴))) |
| 41 | 40 | ralrimiv 3145 |
. . 3
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ (rank‘𝐴)) |
| 42 | | eleq2 2830 |
. . . . 5
⊢ (𝑥 = (rank‘𝐴) → ((rank‘𝑦) ∈ 𝑥 ↔ (rank‘𝑦) ∈ (rank‘𝐴))) |
| 43 | 42 | ralbidv 3178 |
. . . 4
⊢ (𝑥 = (rank‘𝐴) → (∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 (rank‘𝑦) ∈ (rank‘𝐴))) |
| 44 | 43 | onintss 6435 |
. . 3
⊢
((rank‘𝐴)
∈ On → (∀𝑦
∈ 𝐴 (rank‘𝑦) ∈ (rank‘𝐴) → ∩ {𝑥
∈ On ∣ ∀𝑦
∈ 𝐴 (rank‘𝑦) ∈ 𝑥} ⊆ (rank‘𝐴))) |
| 45 | 1, 41, 44 | mpsyl 68 |
. 2
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → ∩ {𝑥
∈ On ∣ ∀𝑦
∈ 𝐴 (rank‘𝑦) ∈ 𝑥} ⊆ (rank‘𝐴)) |
| 46 | 39, 45 | eqssd 4001 |
1
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) →
(rank‘𝐴) = ∩ {𝑥
∈ On ∣ ∀𝑦
∈ 𝐴 (rank‘𝑦) ∈ 𝑥}) |