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 ∧ ( 𝐴 ∩ 𝐶 ) ≺ ( 𝐵 ∩ 𝐶 ) ) → 𝐴 ∈ 𝐵 )