Metamath Proof Explorer

Theorem domssl

Description: If A is a subset of B and C dominates B , then C also dominates A . (Contributed by BTernaryTau, 7-Dec-2024)

Ref Expression
Assertion domssl ⊢ A ⊆ B ∧ B ≼ C → A ≼ C

Proof

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