enpr2dOLD

Description: Obsolete version of enpr2d as of 23-Dec-2024. (Contributed by Rohan Ridenour, 3-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	enpr2dOLD.1	$⊢ φ \to A \in C$
	enpr2dOLD.2	$⊢ φ \to B \in D$
	enpr2dOLD.3	$⊢ φ \to \neg A = B$
Assertion	enpr2dOLD	$⊢ φ \to \{A, B\} \approx 2_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		enpr2dOLD.1	$⊢ φ \to A \in C$
2		enpr2dOLD.2	$⊢ φ \to B \in D$
3		enpr2dOLD.3	$⊢ φ \to \neg A = B$
4		ensn1g	$⊢ A \in C \to \{A\} \approx 1_{𝑜}$
5	1 4	syl	$⊢ φ \to \{A\} \approx 1_{𝑜}$
6		1on	$⊢ 1_{𝑜} \in On$
7		en2sn	$⊢ (B \in D \land 1_{𝑜} \in On) \to \{B\} \approx \{1_{𝑜}\}$
8	2 6 7	sylancl	$⊢ φ \to \{B\} \approx \{1_{𝑜}\}$
9	3	neqned	$⊢ φ \to A \neq B$
10		disjsn2	$⊢ A \neq B \to \{A\} \cap \{B\} = \emptyset$
11	9 10	syl	$⊢ φ \to \{A\} \cap \{B\} = \emptyset$
12	6	onirri	$⊢ \neg 1_{𝑜} \in 1_{𝑜}$
13	12	a1i	$⊢ φ \to \neg 1_{𝑜} \in 1_{𝑜}$
14		disjsn	$⊢ 1_{𝑜} \cap \{1_{𝑜}\} = \emptyset \leftrightarrow \neg 1_{𝑜} \in 1_{𝑜}$
15	13 14	sylibr	$⊢ φ \to 1_{𝑜} \cap \{1_{𝑜}\} = \emptyset$
16		unen	$⊢ ((\{A\} \approx 1_{𝑜} \land \{B\} \approx \{1_{𝑜}\}) \land (\{A\} \cap \{B\} = \emptyset \land 1_{𝑜} \cap \{1_{𝑜}\} = \emptyset)) \to (\{A\} \cup \{B\}) \approx (1_{𝑜} \cup \{1_{𝑜}\})$
17	5 8 11 15 16	syl22anc	$⊢ φ \to (\{A\} \cup \{B\}) \approx (1_{𝑜} \cup \{1_{𝑜}\})$
18		df-pr	$⊢ \{A, B\} = \{A\} \cup \{B\}$
19		df-suc	$⊢ suc 1_{𝑜} = 1_{𝑜} \cup \{1_{𝑜}\}$
20	17 18 19	3brtr4g	$⊢ φ \to \{A, B\} \approx suc 1_{𝑜}$
21		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
22	20 21	breqtrrdi	$⊢ φ \to \{A, B\} \approx 2_{𝑜}$

Metamath Proof Explorer

Theorem enpr2dOLD

Proof