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 ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≼ 𝐶 )

Proof

Step Hyp Ref Expression
1 brdomi ⊢ ( 𝐴 ≼ 𝐵 → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
2 1 3ad2ant3 ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵 ) → ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
3 simp2 ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵 ) → 𝐵 ⊆ 𝐶 )
4 reldom ⊢ Rel ≼
5 4 brrelex1i ⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
6 5 3ad2ant3 ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ∈ V )
7 simp1 ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵 ) → 𝐶 ∈ 𝑉 )
8 3 6 7 jca32 ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 ⊆ 𝐶 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) ) )
9 f1ss ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) → 𝑓 : 𝐴 –1-1→ 𝐶 )
10 vex ⊢ 𝑓 ∈ V
11 f1dom4g ⊢ ( ( ( 𝑓 ∈ V ∧ 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
12 10 11 mp3anl1 ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) ∧ 𝑓 : 𝐴 –1-1→ 𝐶 ) → 𝐴 ≼ 𝐶 )
13 12 ancoms ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐶 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ≼ 𝐶 )
14 9 13 sylan ⊢ ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ⊆ 𝐶 ) ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ≼ 𝐶 )
15 14 expl ⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → ( ( 𝐵 ⊆ 𝐶 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ≼ 𝐶 ) )
16 15 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 → ( ( 𝐵 ⊆ 𝐶 ∧ ( 𝐴 ∈ V ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ≼ 𝐶 ) )
17 2 8 16 sylc ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≼ 𝐶 )