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

Metamath Proof Explorer

Theorem infdjuabs

Description: Absorption law for addition to an infinite cardinal. (Contributed by NM, 30-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infdjuabs ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ≼ 𝐴 )
2 reldom ⊢ Rel ≼
3 2 brrelex2i ⊢ ( 𝐵 ≼ 𝐴 → 𝐴 ∈ V )
4 djudom2 ⊢ ( ( 𝐵 ≼ 𝐴 ∧ 𝐴 ∈ V ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐴 ) )
5 1 3 4 syl2anc2 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐴 ) )
6 xp2dju ⊢ ( 2o × 𝐴 ) = ( 𝐴 ⊔ 𝐴 )
7 5 6 breqtrrdi ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 2o × 𝐴 ) )
8 simp1 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ∈ dom card )
9 2onn ⊢ 2o ∈ ω
10 nnsdom ⊢ ( 2o ∈ ω → 2o ≺ ω )
11 sdomdom ⊢ ( 2o ≺ ω → 2o ≼ ω )
12 9 10 11 mp2b ⊢ 2o ≼ ω
13 simp2 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ω ≼ 𝐴 )
14 domtr ⊢ ( ( 2o ≼ ω ∧ ω ≼ 𝐴 ) → 2o ≼ 𝐴 )
15 12 13 14 sylancr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 2o ≼ 𝐴 )
16 xpdom1g ⊢ ( ( 𝐴 ∈ dom card ∧ 2o ≼ 𝐴 ) → ( 2o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
17 8 15 16 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 2o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
18 domtr ⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( 2o × 𝐴 ) ∧ ( 2o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) )
19 7 17 18 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) )
20 infxpidm2 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
21 20 3adant3 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
22 domentr ⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ≈ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ 𝐴 )
23 19 21 22 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≼ 𝐴 )
24 2 brrelex1i ⊢ ( 𝐵 ≼ 𝐴 → 𝐵 ∈ V )
25 24 3ad2ant3 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ V )
26 djudoml ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ V ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )
27 8 25 26 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) )
28 sbth ⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ≼ 𝐴 ∧ 𝐴 ≼ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ≈ 𝐴 )
29 23 27 28 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ∧ 𝐵 ≼ 𝐴 ) → ( 𝐴 ⊔ 𝐵 ) ≈ 𝐴 )