Proof of Theorem nntr2
Step | Hyp | Ref
| Expression |
1 | | nnon 4605 |
. . . . 5
⊢ (𝐶 ∈ ω → 𝐶 ∈ On) |
2 | 1 | ad3antlr 493 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ On) |
3 | | simpr 110 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵) |
4 | | simprr 531 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) → 𝐵 ∈ 𝐶) |
5 | 4 | adantr 276 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐴 ∈ 𝐵) → 𝐵 ∈ 𝐶) |
6 | 3, 5 | jca 306 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶)) |
7 | | ontr1 4385 |
. . . 4
⊢ (𝐶 ∈ On → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
8 | 2, 6, 7 | sylc 62 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐶) |
9 | | simpr 110 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
10 | 4 | adantr 276 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐴 = 𝐵) → 𝐵 ∈ 𝐶) |
11 | 9, 10 | eqeltrd 2254 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝐶) |
12 | | simplrl 535 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐵 ∈ 𝐴) → 𝐴 ⊆ 𝐵) |
13 | | simpr 110 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴) |
14 | 12, 13 | sseldd 3156 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐵) |
15 | | simplr 528 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) → 𝐶 ∈ ω) |
16 | | elnn 4601 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝐶 ∧ 𝐶 ∈ ω) → 𝐵 ∈ ω) |
17 | 4, 15, 16 | syl2anc 411 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) → 𝐵 ∈ ω) |
18 | 17 | adantr 276 |
. . . . 5
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ ω) |
19 | | nnord 4607 |
. . . . 5
⊢ (𝐵 ∈ ω → Ord 𝐵) |
20 | | ordirr 4537 |
. . . . 5
⊢ (Ord
𝐵 → ¬ 𝐵 ∈ 𝐵) |
21 | 18, 19, 20 | 3syl 17 |
. . . 4
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵 ∈ 𝐵) |
22 | 14, 21 | pm2.21dd 620 |
. . 3
⊢ ((((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) ∧ 𝐵 ∈ 𝐴) → 𝐴 ∈ 𝐶) |
23 | | simpll 527 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) → 𝐴 ∈ ω) |
24 | | nntri3or 6487 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |
25 | 23, 17, 24 | syl2anc 411 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |
26 | 8, 11, 22, 25 | mpjao3dan 1307 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶)) → 𝐴 ∈ 𝐶) |
27 | 26 | ex 115 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |