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	$⊢ (A \in V \land \neg A \in A) \to (A ⊔︀ 1_{𝑜}) \approx suc A$

Proof

Step	Hyp	Ref	Expression
1		enrefg	$⊢ A \in V \to A \approx A$
2	1	adantr	$⊢ (A \in V \land \neg A \in A) \to A \approx A$
3		ensn1g	$⊢ A \in V \to \{A\} \approx 1_{𝑜}$
4	3	ensymd	$⊢ A \in V \to 1_{𝑜} \approx \{A\}$
5	4	adantr	$⊢ (A \in V \land \neg A \in A) \to 1_{𝑜} \approx \{A\}$
6		disjsn	$⊢ A \cap \{A\} = \emptyset \leftrightarrow \neg A \in A$
7	6	bilanri	$⊢ (A \in V \land \neg A \in A) \to A \cap \{A\} = \emptyset$
8		djuenun	$⊢ (A \approx A \land 1_{𝑜} \approx \{A\} \land A \cap \{A\} = \emptyset) \to (A ⊔︀ 1_{𝑜}) \approx (A \cup \{A\})$
9	2 5 7 8	syl3anc	$⊢ (A \in V \land \neg A \in A) \to (A ⊔︀ 1_{𝑜}) \approx (A \cup \{A\})$
10		df-suc	$⊢ suc A = A \cup \{A\}$
11	9 10	breqtrrdi	$⊢ (A \in V \land \neg A \in A) \to (A ⊔︀ 1_{𝑜}) \approx suc A$