Step | Hyp | Ref
| Expression |
1 | | eluni2 3584 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝐴
↔ ∃𝑦 ∈
𝐴 𝑥 ∈ 𝑦) |
2 | | ssel 2939 |
. . . . . . . . 9
⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → 𝑦 ∈ On)) |
3 | | onelss 4124 |
. . . . . . . . 9
⊢ (𝑦 ∈ On → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦)) |
4 | 2, 3 | syl6 29 |
. . . . . . . 8
⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦))) |
5 | | anc2r 311 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ 𝑦)) → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → (𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴)))) |
6 | 4, 5 | syl 14 |
. . . . . . 7
⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → (𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴)))) |
7 | | ssuni 3602 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑥 ⊆ ∪ 𝐴) |
8 | 6, 7 | syl8 65 |
. . . . . 6
⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴))) |
9 | 8 | rexlimdv 2432 |
. . . . 5
⊢ (𝐴 ⊆ On → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ⊆ ∪ 𝐴)) |
10 | 1, 9 | syl5bi 141 |
. . . 4
⊢ (𝐴 ⊆ On → (𝑥 ∈ ∪ 𝐴
→ 𝑥 ⊆ ∪ 𝐴)) |
11 | 10 | ralrimiv 2391 |
. . 3
⊢ (𝐴 ⊆ On → ∀𝑥 ∈ ∪ 𝐴𝑥 ⊆ ∪ 𝐴) |
12 | | dftr3 3858 |
. . 3
⊢ (Tr ∪ 𝐴
↔ ∀𝑥 ∈
∪ 𝐴𝑥 ⊆ ∪ 𝐴) |
13 | 11, 12 | sylibr 137 |
. 2
⊢ (𝐴 ⊆ On → Tr ∪ 𝐴) |
14 | | onelon 4121 |
. . . . . . 7
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → 𝑥 ∈ On) |
15 | 14 | ex 108 |
. . . . . 6
⊢ (𝑦 ∈ On → (𝑥 ∈ 𝑦 → 𝑥 ∈ On)) |
16 | 2, 15 | syl6 29 |
. . . . 5
⊢ (𝐴 ⊆ On → (𝑦 ∈ 𝐴 → (𝑥 ∈ 𝑦 → 𝑥 ∈ On))) |
17 | 16 | rexlimdv 2432 |
. . . 4
⊢ (𝐴 ⊆ On → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → 𝑥 ∈ On)) |
18 | 1, 17 | syl5bi 141 |
. . 3
⊢ (𝐴 ⊆ On → (𝑥 ∈ ∪ 𝐴
→ 𝑥 ∈
On)) |
19 | 18 | ssrdv 2951 |
. 2
⊢ (𝐴 ⊆ On → ∪ 𝐴
⊆ On) |
20 | | ordon 4212 |
. . 3
⊢ Ord
On |
21 | | trssord 4117 |
. . . 4
⊢ ((Tr
∪ 𝐴 ∧ ∪ 𝐴 ⊆ On ∧ Ord On) →
Ord ∪ 𝐴) |
22 | 21 | 3exp 1103 |
. . 3
⊢ (Tr ∪ 𝐴
→ (∪ 𝐴 ⊆ On → (Ord On → Ord ∪ 𝐴))) |
23 | 20, 22 | mpii 39 |
. 2
⊢ (Tr ∪ 𝐴
→ (∪ 𝐴 ⊆ On → Ord ∪ 𝐴)) |
24 | 13, 19, 23 | sylc 56 |
1
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |