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