Proof of Theorem smoword
Step | Hyp | Ref
| Expression |
1 | | smoord 7462 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐷 ∈ 𝐶 ↔ (𝐹‘𝐷) ∈ (𝐹‘𝐶))) |
2 | 1 | notbid 308 |
. . 3
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (¬ 𝐷 ∈ 𝐶 ↔ ¬ (𝐹‘𝐷) ∈ (𝐹‘𝐶))) |
3 | 2 | ancom2s 844 |
. 2
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (¬ 𝐷 ∈ 𝐶 ↔ ¬ (𝐹‘𝐷) ∈ (𝐹‘𝐶))) |
4 | | smodm2 7452 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴) |
5 | 4 | adantr 481 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → Ord 𝐴) |
6 | | simprl 794 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝐶 ∈ 𝐴) |
7 | | ordelord 5745 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝐶 ∈ 𝐴) → Ord 𝐶) |
8 | 5, 6, 7 | syl2anc 693 |
. . 3
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → Ord 𝐶) |
9 | | simprr 796 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → 𝐷 ∈ 𝐴) |
10 | | ordelord 5745 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝐷 ∈ 𝐴) → Ord 𝐷) |
11 | 5, 9, 10 | syl2anc 693 |
. . 3
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → Ord 𝐷) |
12 | | ordtri1 5756 |
. . 3
⊢ ((Ord
𝐶 ∧ Ord 𝐷) → (𝐶 ⊆ 𝐷 ↔ ¬ 𝐷 ∈ 𝐶)) |
13 | 8, 11, 12 | syl2anc 693 |
. 2
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ⊆ 𝐷 ↔ ¬ 𝐷 ∈ 𝐶)) |
14 | | simplr 792 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → Smo 𝐹) |
15 | | smofvon2 7453 |
. . . 4
⊢ (Smo
𝐹 → (𝐹‘𝐶) ∈ On) |
16 | | eloni 5733 |
. . . 4
⊢ ((𝐹‘𝐶) ∈ On → Ord (𝐹‘𝐶)) |
17 | 14, 15, 16 | 3syl 18 |
. . 3
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → Ord (𝐹‘𝐶)) |
18 | | smofvon2 7453 |
. . . 4
⊢ (Smo
𝐹 → (𝐹‘𝐷) ∈ On) |
19 | | eloni 5733 |
. . . 4
⊢ ((𝐹‘𝐷) ∈ On → Ord (𝐹‘𝐷)) |
20 | 14, 18, 19 | 3syl 18 |
. . 3
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → Ord (𝐹‘𝐷)) |
21 | | ordtri1 5756 |
. . 3
⊢ ((Ord
(𝐹‘𝐶) ∧ Ord (𝐹‘𝐷)) → ((𝐹‘𝐶) ⊆ (𝐹‘𝐷) ↔ ¬ (𝐹‘𝐷) ∈ (𝐹‘𝐶))) |
22 | 17, 20, 21 | syl2anc 693 |
. 2
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) ⊆ (𝐹‘𝐷) ↔ ¬ (𝐹‘𝐷) ∈ (𝐹‘𝐶))) |
23 | 3, 13, 22 | 3bitr4d 300 |
1
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ⊆ 𝐷 ↔ (𝐹‘𝐶) ⊆ (𝐹‘𝐷))) |