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

Metamath Proof Explorer

Theorem infunsdom1

Description: The union of two sets that are strictly dominated by the infinite set X is also dominated by X . This version of infunsdom assumes additionally that A is the smaller of the two. (Contributed by Mario Carneiro, 14-Dec-2013) (Revised by Mario Carneiro, 3-May-2015)

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

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) → 𝐴 ≼ 𝐵 )
2 domsdomtr ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ ω ) → 𝐴 ≺ ω )
3 1 2 sylan ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ 𝐵 ≺ ω ) → 𝐴 ≺ ω )
4 unfi2 ⊢ ( ( 𝐴 ≺ ω ∧ 𝐵 ≺ ω ) → ( 𝐴 ∪ 𝐵 ) ≺ ω )
5 3 4 sylancom ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ 𝐵 ≺ ω ) → ( 𝐴 ∪ 𝐵 ) ≺ ω )
6 simpllr ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ 𝐵 ≺ ω ) → ω ≼ 𝑋 )
7 sdomdomtr ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≺ ω ∧ ω ≼ 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
8 5 6 7 syl2anc ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ 𝐵 ≺ ω ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
9 omelon ⊢ ω ∈ On
10 onenon ⊢ ( ω ∈ On → ω ∈ dom card )
11 9 10 ax-mp ⊢ ω ∈ dom card
12 simpll ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) → 𝑋 ∈ dom card )
13 sdomdom ⊢ ( 𝐵 ≺ 𝑋 → 𝐵 ≼ 𝑋 )
14 13 ad2antll ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) → 𝐵 ≼ 𝑋 )
15 numdom ⊢ ( ( 𝑋 ∈ dom card ∧ 𝐵 ≼ 𝑋 ) → 𝐵 ∈ dom card )
16 12 14 15 syl2anc ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) → 𝐵 ∈ dom card )
17 domtri2 ⊢ ( ( ω ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ω ≼ 𝐵 ↔ ¬ 𝐵 ≺ ω ) )
18 11 16 17 sylancr ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) → ( ω ≼ 𝐵 ↔ ¬ 𝐵 ≺ ω ) )
19 18 biimpar ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ¬ 𝐵 ≺ ω ) → ω ≼ 𝐵 )
20 uncom ⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐵 ∪ 𝐴 )
21 16 adantr ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ω ≼ 𝐵 ) → 𝐵 ∈ dom card )
22 simpr ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ω ≼ 𝐵 ) → ω ≼ 𝐵 )
23 1 adantr ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ω ≼ 𝐵 ) → 𝐴 ≼ 𝐵 )
24 infunabs ⊢ ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐵 ∪ 𝐴 ) ≈ 𝐵 )
25 21 22 23 24 syl3anc ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ω ≼ 𝐵 ) → ( 𝐵 ∪ 𝐴 ) ≈ 𝐵 )
26 20 25 eqbrtrid ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ω ≼ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≈ 𝐵 )
27 simplrr ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ω ≼ 𝐵 ) → 𝐵 ≺ 𝑋 )
28 ensdomtr ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ≈ 𝐵 ∧ 𝐵 ≺ 𝑋 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
29 26 27 28 syl2anc ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ω ≼ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
30 19 29 syldan ⊢ ( ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) ∧ ¬ 𝐵 ≺ ω ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )
31 8 30 pm2.61dan ⊢ ( ( ( 𝑋 ∈ dom card ∧ ω ≼ 𝑋 ) ∧ ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝑋 ) ) → ( 𝐴 ∪ 𝐵 ) ≺ 𝑋 )