Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐵 ≼ 𝐶 ) |
2 |
|
reldom |
⊢ Rel ≼ |
3 |
2
|
brrelex12i |
⊢ ( 𝐵 ≼ 𝐶 → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) |
4 |
|
simpl |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ⊆ 𝐵 ) |
5 |
|
ssexg |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V ) |
6 |
5
|
adantrr |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ∈ V ) |
7 |
|
simprr |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐶 ∈ V ) |
8 |
4 6 7
|
jca32 |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) ) → ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) ) |
9 |
3 8
|
sylan2 |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) ) |
10 |
|
brdomi |
⊢ ( 𝐵 ≼ 𝐶 → ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 ) |
11 |
|
f1ssres |
⊢ ( ( 𝑓 : 𝐵 –1-1→ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑓 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐶 ) |
12 |
|
vex |
⊢ 𝑓 ∈ V |
13 |
12
|
resex |
⊢ ( 𝑓 ↾ 𝐴 ) ∈ V |
14 |
|
f1dom4g |
⊢ ( ( ( ( 𝑓 ↾ 𝐴 ) ∈ V ∧ 𝐴 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝑓 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 ) |
15 |
13 14
|
mp3anl1 |
⊢ ( ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ∧ ( 𝑓 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 ) |
16 |
15
|
ancoms |
⊢ ( ( ( 𝑓 ↾ 𝐴 ) : 𝐴 –1-1→ 𝐶 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 ) |
17 |
11 16
|
sylan |
⊢ ( ( ( 𝑓 : 𝐵 –1-1→ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 ) |
18 |
17
|
expl |
⊢ ( 𝑓 : 𝐵 –1-1→ 𝐶 → ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 ) ) |
19 |
18
|
exlimiv |
⊢ ( ∃ 𝑓 𝑓 : 𝐵 –1-1→ 𝐶 → ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 ) ) |
20 |
10 19
|
syl |
⊢ ( 𝐵 ≼ 𝐶 → ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) ) → 𝐴 ≼ 𝐶 ) ) |
21 |
1 9 20
|
sylc |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 ) |