Metamath Proof Explorer


Theorem dju1en

Description: Cardinal addition with cardinal one (which is the same as ordinal one). Used in proof of Theorem 6J of Enderton p. 143. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion dju1en ( ( 𝐴𝑉 ∧ ¬ 𝐴𝐴 ) → ( 𝐴 ⊔ 1o ) ≈ suc 𝐴 )

Proof

Step Hyp Ref Expression
1 enrefg ( 𝐴𝑉𝐴𝐴 )
2 1 adantr ( ( 𝐴𝑉 ∧ ¬ 𝐴𝐴 ) → 𝐴𝐴 )
3 ensn1g ( 𝐴𝑉 → { 𝐴 } ≈ 1o )
4 3 ensymd ( 𝐴𝑉 → 1o ≈ { 𝐴 } )
5 4 adantr ( ( 𝐴𝑉 ∧ ¬ 𝐴𝐴 ) → 1o ≈ { 𝐴 } )
6 simpr ( ( 𝐴𝑉 ∧ ¬ 𝐴𝐴 ) → ¬ 𝐴𝐴 )
7 disjsn ( ( 𝐴 ∩ { 𝐴 } ) = ∅ ↔ ¬ 𝐴𝐴 )
8 6 7 sylibr ( ( 𝐴𝑉 ∧ ¬ 𝐴𝐴 ) → ( 𝐴 ∩ { 𝐴 } ) = ∅ )
9 djuenun ( ( 𝐴𝐴 ∧ 1o ≈ { 𝐴 } ∧ ( 𝐴 ∩ { 𝐴 } ) = ∅ ) → ( 𝐴 ⊔ 1o ) ≈ ( 𝐴 ∪ { 𝐴 } ) )
10 2 5 8 9 syl3anc ( ( 𝐴𝑉 ∧ ¬ 𝐴𝐴 ) → ( 𝐴 ⊔ 1o ) ≈ ( 𝐴 ∪ { 𝐴 } ) )
11 df-suc suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
12 10 11 breqtrrdi ( ( 𝐴𝑉 ∧ ¬ 𝐴𝐴 ) → ( 𝐴 ⊔ 1o ) ≈ suc 𝐴 )