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