Metamath Proof Explorer

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	$⊢ (A \in ω \land B \in ω) \to card ((A ⊔︀ B)) = A +_{𝑜} B$

Proof

Step	Hyp	Ref	Expression
1		nnon	$⊢ A \in ω \to A \in On$
2		nnon	$⊢ B \in ω \to B \in On$
3		onadju	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B) \approx (A ⊔︀ B)$
4	1 2 3	syl2an	$⊢ (A \in ω \land B \in ω) \to (A +_{𝑜} B) \approx (A ⊔︀ B)$
5		carden2b	$⊢ (A +_{𝑜} B) \approx (A ⊔︀ B) \to card (A +_{𝑜} B) = card ((A ⊔︀ B))$
6	4 5	syl	$⊢ (A \in ω \land B \in ω) \to card (A +_{𝑜} B) = card ((A ⊔︀ B))$
7		nnacl	$⊢ (A \in ω \land B \in ω) \to A +_{𝑜} B \in ω$
8		cardnn	$⊢ A +_{𝑜} B \in ω \to card (A +_{𝑜} B) = A +_{𝑜} B$
9	7 8	syl	$⊢ (A \in ω \land B \in ω) \to card (A +_{𝑜} B) = A +_{𝑜} B$
10	6 9	eqtr3d	$⊢ (A \in ω \land B \in ω) \to card ((A ⊔︀ B)) = A +_{𝑜} B$