| Step | Hyp | Ref
| Expression |
| 1 | | unwf 9850 |
. . . . . . 7
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) ↔ (𝐴 ∪ 𝐵) ∈ ∪
(𝑅1 “ On)) |
| 2 | | rankval3b 9866 |
. . . . . . 7
⊢ ((𝐴 ∪ 𝐵) ∈ ∪
(𝑅1 “ On) → (rank‘(𝐴 ∪ 𝐵)) = ∩ {𝑦 ∈ On ∣ ∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦}) |
| 3 | 1, 2 | sylbi 217 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) →
(rank‘(𝐴 ∪ 𝐵)) = ∩ {𝑦
∈ On ∣ ∀𝑥
∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦}) |
| 4 | 3 | eleq2d 2827 |
. . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (𝑥 ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ 𝑥 ∈ ∩ {𝑦 ∈ On ∣ ∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦})) |
| 5 | | vex 3484 |
. . . . . 6
⊢ 𝑥 ∈ V |
| 6 | 5 | elintrab 4960 |
. . . . 5
⊢ (𝑥 ∈ ∩ {𝑦
∈ On ∣ ∀𝑥
∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦} ↔ ∀𝑦 ∈ On (∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦 → 𝑥 ∈ 𝑦)) |
| 7 | 4, 6 | bitrdi 287 |
. . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (𝑥 ∈ (rank‘(𝐴 ∪ 𝐵)) ↔ ∀𝑦 ∈ On (∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦 → 𝑥 ∈ 𝑦))) |
| 8 | | elun 4153 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
| 9 | | rankelb 9864 |
. . . . . . . . 9
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ (rank‘𝐴))) |
| 10 | | elun1 4182 |
. . . . . . . . 9
⊢
((rank‘𝑥)
∈ (rank‘𝐴)
→ (rank‘𝑥)
∈ ((rank‘𝐴)
∪ (rank‘𝐵))) |
| 11 | 9, 10 | syl6 35 |
. . . . . . . 8
⊢ (𝐴 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐴 → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 12 | | rankelb 9864 |
. . . . . . . . 9
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐵 → (rank‘𝑥) ∈ (rank‘𝐵))) |
| 13 | | elun2 4183 |
. . . . . . . . 9
⊢
((rank‘𝑥)
∈ (rank‘𝐵)
→ (rank‘𝑥)
∈ ((rank‘𝐴)
∪ (rank‘𝐵))) |
| 14 | 12, 13 | syl6 35 |
. . . . . . . 8
⊢ (𝐵 ∈ ∪ (𝑅1 “ On) → (𝑥 ∈ 𝐵 → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 15 | 11, 14 | jaao 957 |
. . . . . . 7
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 16 | 8, 15 | biimtrid 242 |
. . . . . 6
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (𝑥 ∈ (𝐴 ∪ 𝐵) → (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 17 | 16 | ralrimiv 3145 |
. . . . 5
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → ∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵))) |
| 18 | | rankon 9835 |
. . . . . . 7
⊢
(rank‘𝐴)
∈ On |
| 19 | | rankon 9835 |
. . . . . . 7
⊢
(rank‘𝐵)
∈ On |
| 20 | 18, 19 | onun2i 6506 |
. . . . . 6
⊢
((rank‘𝐴)
∪ (rank‘𝐵))
∈ On |
| 21 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑦 = ((rank‘𝐴) ∪ (rank‘𝐵)) → ((rank‘𝑥) ∈ 𝑦 ↔ (rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 22 | 21 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑦 = ((rank‘𝐴) ∪ (rank‘𝐵)) → (∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦 ↔ ∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 23 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑦 = ((rank‘𝐴) ∪ (rank‘𝐵)) → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 24 | 22, 23 | imbi12d 344 |
. . . . . . 7
⊢ (𝑦 = ((rank‘𝐴) ∪ (rank‘𝐵)) → ((∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦 → 𝑥 ∈ 𝑦) ↔ (∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))) |
| 25 | 24 | rspcv 3618 |
. . . . . 6
⊢
(((rank‘𝐴)
∪ (rank‘𝐵))
∈ On → (∀𝑦
∈ On (∀𝑥 ∈
(𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦 → 𝑥 ∈ 𝑦) → (∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵))))) |
| 26 | 20, 25 | ax-mp 5 |
. . . . 5
⊢
(∀𝑦 ∈ On
(∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦 → 𝑥 ∈ 𝑦) → (∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ ((rank‘𝐴) ∪ (rank‘𝐵)) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 27 | 17, 26 | syl5com 31 |
. . . 4
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) →
(∀𝑦 ∈ On
(∀𝑥 ∈ (𝐴 ∪ 𝐵)(rank‘𝑥) ∈ 𝑦 → 𝑥 ∈ 𝑦) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 28 | 7, 27 | sylbid 240 |
. . 3
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) → (𝑥 ∈ (rank‘(𝐴 ∪ 𝐵)) → 𝑥 ∈ ((rank‘𝐴) ∪ (rank‘𝐵)))) |
| 29 | 28 | ssrdv 3989 |
. 2
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) →
(rank‘(𝐴 ∪ 𝐵)) ⊆ ((rank‘𝐴) ∪ (rank‘𝐵))) |
| 30 | | ssun1 4178 |
. . . . 5
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
| 31 | | rankssb 9888 |
. . . . 5
⊢ ((𝐴 ∪ 𝐵) ∈ ∪
(𝑅1 “ On) → (𝐴 ⊆ (𝐴 ∪ 𝐵) → (rank‘𝐴) ⊆ (rank‘(𝐴 ∪ 𝐵)))) |
| 32 | 30, 31 | mpi 20 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) ∈ ∪
(𝑅1 “ On) → (rank‘𝐴) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
| 33 | | ssun2 4179 |
. . . . 5
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
| 34 | | rankssb 9888 |
. . . . 5
⊢ ((𝐴 ∪ 𝐵) ∈ ∪
(𝑅1 “ On) → (𝐵 ⊆ (𝐴 ∪ 𝐵) → (rank‘𝐵) ⊆ (rank‘(𝐴 ∪ 𝐵)))) |
| 35 | 33, 34 | mpi 20 |
. . . 4
⊢ ((𝐴 ∪ 𝐵) ∈ ∪
(𝑅1 “ On) → (rank‘𝐵) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
| 36 | 32, 35 | unssd 4192 |
. . 3
⊢ ((𝐴 ∪ 𝐵) ∈ ∪
(𝑅1 “ On) → ((rank‘𝐴) ∪ (rank‘𝐵)) ⊆ (rank‘(𝐴 ∪ 𝐵))) |
| 37 | 1, 36 | sylbi 217 |
. 2
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) →
((rank‘𝐴) ∪
(rank‘𝐵)) ⊆
(rank‘(𝐴 ∪ 𝐵))) |
| 38 | 29, 37 | eqssd 4001 |
1
⊢ ((𝐴 ∈ ∪ (𝑅1 “ On) ∧ 𝐵 ∈ ∪ (𝑅1 “ On)) →
(rank‘(𝐴 ∪ 𝐵)) = ((rank‘𝐴) ∪ (rank‘𝐵))) |