Metamath Proof Explorer

Theorem infunsdom

Description: The union of two sets that are strictly dominated by the infinite set X is also strictly dominated by X . (Contributed by Mario Carneiro, 3-May-2015)

Ref Expression
Assertion infunsdom ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
2 infunsdom1 ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
3 2 anass1rs ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝐵 ≺ 𝑋 ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
4 3 adantlrl ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
5 1 4 sylan2 ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) ∧ 𝐴 ≺ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
6 simpll ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) → 𝑋 ∈ dom card )
7 sdomdom ⊢ ( 𝐵 ≺ 𝑋 → 𝐵 ≼ 𝑋 )
8 7 ad2antll ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) → 𝐵 ≼ 𝑋 )
9 numdom ⊢ ( ( 𝑋 ∈ dom card ∧ 𝐵 ≼ 𝑋 ) → 𝐵 ∈ dom card )
10 6 8 9 syl2anc ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) → 𝐵 ∈ dom card )
11 sdomdom ⊢ ( 𝐴 ≺ 𝑋 → 𝐴 ≼ 𝑋 )
12 11 ad2antrl ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) → 𝐴 ≼ 𝑋 )
13 numdom ⊢ ( ( 𝑋 ∈ dom card ∧ 𝐴 ≼ 𝑋 ) → 𝐴 ∈ dom card )
14 6 12 13 syl2anc ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) → 𝐴 ∈ dom card )
15 domtri2 ⊢ ( ( 𝐵 ∈ dom card ∧ 𝐴 ∈ dom card ) → ( 𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵 ) )
16 10 14 15 syl2anc ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) → ( 𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵 ) )
17 16 biimpar ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ¬ 𝐴 ≺ 𝐵 ) → 𝐵 ≼ 𝐴 )
18 uncom ⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐵 ∪ 𝐴 )
19 infunsdom1 ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐵 ≼ 𝐴 ∧ 𝐴 ≺ 𝑋 ) ) → ( 𝐵 ∪ 𝐴 ) ≺ 𝑋 )
20 18 19 eqbrtrid ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐵 ≼ 𝐴 ∧ 𝐴 ≺ 𝑋 ) ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
21 20 anass1rs ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ 𝐴 ≺ 𝑋 ) ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
22 21 adantlrr ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
23 17 22 syldan ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ¬ 𝐴 ≺ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
24 5 23 pm2.61dan ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≺ 𝑋 ∧ 𝐵 ≺ 𝑋 ) ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )