Theorem nnadjuALT

Description: Shorter proof of nnadju using ax-rep . (Contributed by Paul Chapman, 11-Apr-2009) (Revised by Mario Carneiro, 6-Feb-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nnadjuALT	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴 ⊔ 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
2		nnon	⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
3		onadju	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ≈ ( 𝐴 ⊔ 𝐵 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ≈ ( 𝐴 ⊔ 𝐵 ) )
5		carden2b	⊢ ( ( 𝐴 +o 𝐵 ) ≈ ( 𝐴 ⊔ 𝐵 ) → ( card ‘ ( 𝐴 +o 𝐵 ) ) = ( card ‘ ( 𝐴 ⊔ 𝐵 ) ) )
6	4 5	syl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴 +o 𝐵 ) ) = ( card ‘ ( 𝐴 ⊔ 𝐵 ) ) )
7		nnacl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) ∈ ω )
8		cardnn	⊢ ( ( 𝐴 +o 𝐵 ) ∈ ω → ( card ‘ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )
9	7 8	syl	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )
10	6 9	eqtr3d	⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( card ‘ ( 𝐴 ⊔ 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )