Proof of Theorem onintonm
Step | Hyp | Ref
| Expression |
1 | | ssel 3141 |
. . . . . . 7
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → 𝑥 ∈ On)) |
2 | | eloni 4358 |
. . . . . . . 8
⊢ (𝑥 ∈ On → Ord 𝑥) |
3 | | ordtr 4361 |
. . . . . . . 8
⊢ (Ord
𝑥 → Tr 𝑥) |
4 | 2, 3 | syl 14 |
. . . . . . 7
⊢ (𝑥 ∈ On → Tr 𝑥) |
5 | 1, 4 | syl6 33 |
. . . . . 6
⊢ (𝐴 ⊆ On → (𝑥 ∈ 𝐴 → Tr 𝑥)) |
6 | 5 | ralrimiv 2542 |
. . . . 5
⊢ (𝐴 ⊆ On → ∀𝑥 ∈ 𝐴 Tr 𝑥) |
7 | | trint 4100 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → Tr ∩ 𝐴) |
8 | 6, 7 | syl 14 |
. . . 4
⊢ (𝐴 ⊆ On → Tr ∩ 𝐴) |
9 | 8 | adantr 274 |
. . 3
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → Tr ∩
𝐴) |
10 | | nfv 1521 |
. . . . 5
⊢
Ⅎ𝑥 𝐴 ⊆ On |
11 | | nfe1 1489 |
. . . . 5
⊢
Ⅎ𝑥∃𝑥 𝑥 ∈ 𝐴 |
12 | 10, 11 | nfan 1558 |
. . . 4
⊢
Ⅎ𝑥(𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) |
13 | | intssuni2m 3853 |
. . . . . . . 8
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ ∪ On) |
14 | | unon 4493 |
. . . . . . . 8
⊢ ∪ On = On |
15 | 13, 14 | sseqtrdi 3195 |
. . . . . . 7
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ⊆ On) |
16 | 15 | sseld 3146 |
. . . . . 6
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → (𝑥 ∈ ∩ 𝐴 → 𝑥 ∈ On)) |
17 | 16, 2 | syl6 33 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → (𝑥 ∈ ∩ 𝐴 → Ord 𝑥)) |
18 | 17, 3 | syl6 33 |
. . . 4
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → (𝑥 ∈ ∩ 𝐴 → Tr 𝑥)) |
19 | 12, 18 | ralrimi 2541 |
. . 3
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∀𝑥 ∈ ∩ 𝐴Tr 𝑥) |
20 | | dford3 4350 |
. . 3
⊢ (Ord
∩ 𝐴 ↔ (Tr ∩
𝐴 ∧ ∀𝑥 ∈ ∩ 𝐴Tr
𝑥)) |
21 | 9, 19, 20 | sylanbrc 415 |
. 2
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → Ord ∩
𝐴) |
22 | | inteximm 4133 |
. . . 4
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ V) |
23 | 22 | adantl 275 |
. . 3
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ∈ V) |
24 | | elong 4356 |
. . 3
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ On ↔ Ord ∩ 𝐴)) |
25 | 23, 24 | syl 14 |
. 2
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → (∩ 𝐴 ∈ On ↔ Ord ∩ 𝐴)) |
26 | 21, 25 | mpbird 166 |
1
⊢ ((𝐴 ⊆ On ∧ ∃𝑥 𝑥 ∈ 𝐴) → ∩ 𝐴 ∈ On) |