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

Metamath Proof Explorer

Theorem onsdominel

Description: An ordinal with more elements of some type is larger. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion onsdominel ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ( 𝐴 ∩ 𝐶 ) ≺ ( 𝐵 ∩ 𝐶 ) ) → 𝐴 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ontri1 ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
2 1 ancoms ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
3 inex1g ⊢ ( 𝐴 ∈ On → ( 𝐴 ∩ 𝐶 ) ∈ V )
4 ssrin ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐵 ∩ 𝐶 ) ⊆ ( 𝐴 ∩ 𝐶 ) )
5 ssdomg ⊢ ( ( 𝐴 ∩ 𝐶 ) ∈ V → ( ( 𝐵 ∩ 𝐶 ) ⊆ ( 𝐴 ∩ 𝐶 ) → ( 𝐵 ∩ 𝐶 ) ≼ ( 𝐴 ∩ 𝐶 ) ) )
6 3 4 5 syl2im ⊢ ( 𝐴 ∈ On → ( 𝐵 ⊆ 𝐴 → ( 𝐵 ∩ 𝐶 ) ≼ ( 𝐴 ∩ 𝐶 ) ) )
7 domnsym ⊢ ( ( 𝐵 ∩ 𝐶 ) ≼ ( 𝐴 ∩ 𝐶 ) → ¬ ( 𝐴 ∩ 𝐶 ) ≺ ( 𝐵 ∩ 𝐶 ) )
8 6 7 syl6 ⊢ ( 𝐴 ∈ On → ( 𝐵 ⊆ 𝐴 → ¬ ( 𝐴 ∩ 𝐶 ) ≺ ( 𝐵 ∩ 𝐶 ) ) )
9 8 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐵 ⊆ 𝐴 → ¬ ( 𝐴 ∩ 𝐶 ) ≺ ( 𝐵 ∩ 𝐶 ) ) )
10 2 9 sylbird ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ 𝐴 ∈ 𝐵 → ¬ ( 𝐴 ∩ 𝐶 ) ≺ ( 𝐵 ∩ 𝐶 ) ) )
11 10 con4d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∩ 𝐶 ) ≺ ( 𝐵 ∩ 𝐶 ) → 𝐴 ∈ 𝐵 ) )
12 11 3impia ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ( 𝐴 ∩ 𝐶 ) ≺ ( 𝐵 ∩ 𝐶 ) ) → 𝐴 ∈ 𝐵 )