Step |
Hyp |
Ref |
Expression |
1 |
|
smoord |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐷 ∈ 𝐶 ↔ ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 ‘ 𝐶 ) ) ) |
2 |
1
|
notbid |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( ¬ 𝐷 ∈ 𝐶 ↔ ¬ ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 ‘ 𝐶 ) ) ) |
3 |
2
|
ancom2s |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ¬ 𝐷 ∈ 𝐶 ↔ ¬ ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 ‘ 𝐶 ) ) ) |
4 |
|
smodm2 |
⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → Ord 𝐴 ) |
5 |
|
simprl |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐶 ∈ 𝐴 ) |
6 |
|
ordelord |
⊢ ( ( Ord 𝐴 ∧ 𝐶 ∈ 𝐴 ) → Ord 𝐶 ) |
7 |
4 5 6
|
syl2an2r |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → Ord 𝐶 ) |
8 |
|
simprr |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → 𝐷 ∈ 𝐴 ) |
9 |
|
ordelord |
⊢ ( ( Ord 𝐴 ∧ 𝐷 ∈ 𝐴 ) → Ord 𝐷 ) |
10 |
4 8 9
|
syl2an2r |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → Ord 𝐷 ) |
11 |
|
ordtri1 |
⊢ ( ( Ord 𝐶 ∧ Ord 𝐷 ) → ( 𝐶 ⊆ 𝐷 ↔ ¬ 𝐷 ∈ 𝐶 ) ) |
12 |
7 10 11
|
syl2anc |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 ⊆ 𝐷 ↔ ¬ 𝐷 ∈ 𝐶 ) ) |
13 |
|
simplr |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → Smo 𝐹 ) |
14 |
|
smofvon2 |
⊢ ( Smo 𝐹 → ( 𝐹 ‘ 𝐶 ) ∈ On ) |
15 |
|
eloni |
⊢ ( ( 𝐹 ‘ 𝐶 ) ∈ On → Ord ( 𝐹 ‘ 𝐶 ) ) |
16 |
13 14 15
|
3syl |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → Ord ( 𝐹 ‘ 𝐶 ) ) |
17 |
|
smofvon2 |
⊢ ( Smo 𝐹 → ( 𝐹 ‘ 𝐷 ) ∈ On ) |
18 |
|
eloni |
⊢ ( ( 𝐹 ‘ 𝐷 ) ∈ On → Ord ( 𝐹 ‘ 𝐷 ) ) |
19 |
13 17 18
|
3syl |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → Ord ( 𝐹 ‘ 𝐷 ) ) |
20 |
|
ordtri1 |
⊢ ( ( Ord ( 𝐹 ‘ 𝐶 ) ∧ Ord ( 𝐹 ‘ 𝐷 ) ) → ( ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝐷 ) ↔ ¬ ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 ‘ 𝐶 ) ) ) |
21 |
16 19 20
|
syl2anc |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝐷 ) ↔ ¬ ( 𝐹 ‘ 𝐷 ) ∈ ( 𝐹 ‘ 𝐶 ) ) ) |
22 |
3 12 21
|
3bitr4d |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 ⊆ 𝐷 ↔ ( 𝐹 ‘ 𝐶 ) ⊆ ( 𝐹 ‘ 𝐷 ) ) ) |