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

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 𝐴 )