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 ( ( 𝐴𝐵𝐵𝐶 ) → 𝐴𝐶 )

Proof

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 ( ( 𝐴𝐵𝐵𝐶 ) → 𝐴𝐶 )