This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem domssr

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

Ref Expression
Assertion domssr ⊢ C ∈ V ∧ B ⊆ C ∧ A ≼ B → A ≼ C

Proof

Step Hyp Ref Expression
1 brdomi ⊢ A ≼ B → ∃ f f : A ⟶ 1-1 B
2 1 3ad2ant3 ⊢ C ∈ V ∧ B ⊆ C ∧ A ≼ B → ∃ f f : A ⟶ 1-1 B
3 simp2 ⊢ C ∈ V ∧ B ⊆ C ∧ A ≼ B → B ⊆ C
4 reldom ⊢ Rel ⁡ ≼
5 4 brrelex1i ⊢ A ≼ B → A ∈ V
6 5 3ad2ant3 ⊢ C ∈ V ∧ B ⊆ C ∧ A ≼ B → A ∈ V
7 simp1 ⊢ C ∈ V ∧ B ⊆ C ∧ A ≼ B → C ∈ V
8 3 6 7 jca32 ⊢ C ∈ V ∧ B ⊆ C ∧ A ≼ B → B ⊆ C ∧ A ∈ V ∧ C ∈ V
9 f1ss ⊢ f : A ⟶ 1-1 B ∧ B ⊆ C → f : A ⟶ 1-1 C
10 vex ⊢ f ∈ V
11 f1dom4g ⊢ f ∈ V ∧ A ∈ V ∧ C ∈ V ∧ f : A ⟶ 1-1 C → A ≼ C
12 10 11 mp3anl1 ⊢ A ∈ V ∧ C ∈ V ∧ f : A ⟶ 1-1 C → A ≼ C
13 12 ancoms ⊢ f : A ⟶ 1-1 C ∧ A ∈ V ∧ C ∈ V → A ≼ C
14 9 13 sylan ⊢ f : A ⟶ 1-1 B ∧ B ⊆ C ∧ A ∈ V ∧ C ∈ V → A ≼ C
15 14 expl ⊢ f : A ⟶ 1-1 B → B ⊆ C ∧ A ∈ V ∧ C ∈ V → A ≼ C
16 15 exlimiv ⊢ ∃ f f : A ⟶ 1-1 B → B ⊆ C ∧ A ∈ V ∧ C ∈ V → A ≼ C
17 2 8 16 sylc ⊢ C ∈ V ∧ B ⊆ C ∧ A ≼ B → A ≼ C