Metamath Proof Explorer

Theorem sucxpdom

Description: Cartesian product dominates successor for set with cardinality greater than 1. Proposition 10.38 of TakeutiZaring p. 93 (but generalized to arbitrary sets, not just ordinals). (Contributed by NM, 3-Sep-2004) (Proof shortened by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion sucxpdom ( 1o ≺ 𝐴 → suc 𝐴 ≼ ( 𝐴 × 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
2 relsdom ⊢ Rel ≺
3 2 brrelex2i ⊢ ( 1o ≺ 𝐴 → 𝐴 ∈ V )
4 1on ⊢ 1o ∈ On
5 xpsneng ⊢ ( ( 𝐴 ∈ V ∧ 1o ∈ On ) → ( 𝐴 × { 1o } ) ≈ 𝐴 )
6 3 4 5 sylancl ⊢ ( 1o ≺ 𝐴 → ( 𝐴 × { 1o } ) ≈ 𝐴 )
7 6 ensymd ⊢ ( 1o ≺ 𝐴 → 𝐴 ≈ ( 𝐴 × { 1o } ) )
8 endom ⊢ ( 𝐴 ≈ ( 𝐴 × { 1o } ) → 𝐴 ≼ ( 𝐴 × { 1o } ) )
9 7 8 syl ⊢ ( 1o ≺ 𝐴 → 𝐴 ≼ ( 𝐴 × { 1o } ) )
10 ensn1g ⊢ ( 𝐴 ∈ V → { 𝐴 } ≈ 1o )
11 3 10 syl ⊢ ( 1o ≺ 𝐴 → { 𝐴 } ≈ 1o )
12 ensdomtr ⊢ ( ( { 𝐴 } ≈ 1o ∧ 1o ≺ 𝐴 ) → { 𝐴 } ≺ 𝐴 )
13 11 12 mpancom ⊢ ( 1o ≺ 𝐴 → { 𝐴 } ≺ 𝐴 )
14 0ex ⊢ ∅ ∈ V
15 xpsneng ⊢ ( ( 𝐴 ∈ V ∧ ∅ ∈ V ) → ( 𝐴 × { ∅ } ) ≈ 𝐴 )
16 3 14 15 sylancl ⊢ ( 1o ≺ 𝐴 → ( 𝐴 × { ∅ } ) ≈ 𝐴 )
17 16 ensymd ⊢ ( 1o ≺ 𝐴 → 𝐴 ≈ ( 𝐴 × { ∅ } ) )
18 sdomentr ⊢ ( ( { 𝐴 } ≺ 𝐴 ∧ 𝐴 ≈ ( 𝐴 × { ∅ } ) ) → { 𝐴 } ≺ ( 𝐴 × { ∅ } ) )
19 13 17 18 syl2anc ⊢ ( 1o ≺ 𝐴 → { 𝐴 } ≺ ( 𝐴 × { ∅ } ) )
20 sdomdom ⊢ ( { 𝐴 } ≺ ( 𝐴 × { ∅ } ) → { 𝐴 } ≼ ( 𝐴 × { ∅ } ) )
21 19 20 syl ⊢ ( 1o ≺ 𝐴 → { 𝐴 } ≼ ( 𝐴 × { ∅ } ) )
22 1n0 ⊢ 1o ≠ ∅
23 xpsndisj ⊢ ( 1o ≠ ∅ → ( ( 𝐴 × { 1o } ) ∩ ( 𝐴 × { ∅ } ) ) = ∅ )
24 22 23 mp1i ⊢ ( 1o ≺ 𝐴 → ( ( 𝐴 × { 1o } ) ∩ ( 𝐴 × { ∅ } ) ) = ∅ )
25 undom ⊢ ( ( ( 𝐴 ≼ ( 𝐴 × { 1o } ) ∧ { 𝐴 } ≼ ( 𝐴 × { ∅ } ) ) ∧ ( ( 𝐴 × { 1o } ) ∩ ( 𝐴 × { ∅ } ) ) = ∅ ) → ( 𝐴 ∪ { 𝐴 } ) ≼ ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) )
26 9 21 24 25 syl21anc ⊢ ( 1o ≺ 𝐴 → ( 𝐴 ∪ { 𝐴 } ) ≼ ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) )
27 sdomentr ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐴 ≈ ( 𝐴 × { 1o } ) ) → 1o ≺ ( 𝐴 × { 1o } ) )
28 7 27 mpdan ⊢ ( 1o ≺ 𝐴 → 1o ≺ ( 𝐴 × { 1o } ) )
29 sdomentr ⊢ ( ( 1o ≺ 𝐴 ∧ 𝐴 ≈ ( 𝐴 × { ∅ } ) ) → 1o ≺ ( 𝐴 × { ∅ } ) )
30 17 29 mpdan ⊢ ( 1o ≺ 𝐴 → 1o ≺ ( 𝐴 × { ∅ } ) )
31 unxpdom ⊢ ( ( 1o ≺ ( 𝐴 × { 1o } ) ∧ 1o ≺ ( 𝐴 × { ∅ } ) ) → ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) )
32 28 30 31 syl2anc ⊢ ( 1o ≺ 𝐴 → ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) )
33 domtr ⊢ ( ( ( 𝐴 ∪ { 𝐴 } ) ≼ ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ∧ ( ( 𝐴 × { 1o } ) ∪ ( 𝐴 × { ∅ } ) ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ) → ( 𝐴 ∪ { 𝐴 } ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) )
34 26 32 33 syl2anc ⊢ ( 1o ≺ 𝐴 → ( 𝐴 ∪ { 𝐴 } ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) )
35 xpen ⊢ ( ( ( 𝐴 × { 1o } ) ≈ 𝐴 ∧ ( 𝐴 × { ∅ } ) ≈ 𝐴 ) → ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ≈ ( 𝐴 × 𝐴 ) )
36 6 16 35 syl2anc ⊢ ( 1o ≺ 𝐴 → ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ≈ ( 𝐴 × 𝐴 ) )
37 domentr ⊢ ( ( ( 𝐴 ∪ { 𝐴 } ) ≼ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ∧ ( ( 𝐴 × { 1o } ) × ( 𝐴 × { ∅ } ) ) ≈ ( 𝐴 × 𝐴 ) ) → ( 𝐴 ∪ { 𝐴 } ) ≼ ( 𝐴 × 𝐴 ) )
38 34 36 37 syl2anc ⊢ ( 1o ≺ 𝐴 → ( 𝐴 ∪ { 𝐴 } ) ≼ ( 𝐴 × 𝐴 ) )
39 1 38 eqbrtrid ⊢ ( 1o ≺ 𝐴 → suc 𝐴 ≼ ( 𝐴 × 𝐴 ) )