enrefnn

Description: Equinumerosity is reflexive for finite ordinals, proved without using the Axiom of Power Sets (unlike enrefg ). (Contributed by BTernaryTau, 31-Jul-2024)

		Ref	Expression
	Assertion	enrefnn	$⊢ A \in ω \to A \approx A$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ x = \emptyset \to x = \emptyset$
2	1 1	breq12d	$⊢ x = \emptyset \to (x \approx x \leftrightarrow \emptyset \approx \emptyset)$
3		id	$⊢ x = y \to x = y$
4	3 3	breq12d	$⊢ x = y \to (x \approx x \leftrightarrow y \approx y)$
5		id	$⊢ x = suc y \to x = suc y$
6	5 5	breq12d	$⊢ x = suc y \to (x \approx x \leftrightarrow suc y \approx suc y)$
7		id	$⊢ x = A \to x = A$
8	7 7	breq12d	$⊢ x = A \to (x \approx x \leftrightarrow A \approx A)$
9		eqid	$⊢ \emptyset = \emptyset$
10		en0	$⊢ \emptyset \approx \emptyset \leftrightarrow \emptyset = \emptyset$
11	9 10	mpbir	$⊢ \emptyset \approx \emptyset$
12		en2sn	$⊢ (y \in V \land y \in V) \to \{y\} \approx \{y\}$
13	12	el2v	$⊢ \{y\} \approx \{y\}$
14	13	jctr	$⊢ y \approx y \to (y \approx y \land \{y\} \approx \{y\})$
15		nnord	$⊢ y \in ω \to Ord y$
16		orddisj	$⊢ Ord y \to y \cap \{y\} = \emptyset$
17	15 16	syl	$⊢ y \in ω \to y \cap \{y\} = \emptyset$
18	17 17	jca	$⊢ y \in ω \to (y \cap \{y\} = \emptyset \land y \cap \{y\} = \emptyset)$
19		unen	$⊢ ((y \approx y \land \{y\} \approx \{y\}) \land (y \cap \{y\} = \emptyset \land y \cap \{y\} = \emptyset)) \to (y \cup \{y\}) \approx (y \cup \{y\})$
20	14 18 19	syl2anr	$⊢ (y \in ω \land y \approx y) \to (y \cup \{y\}) \approx (y \cup \{y\})$
21		df-suc	$⊢ suc y = y \cup \{y\}$
22	20 21 21	3brtr4g	$⊢ (y \in ω \land y \approx y) \to suc y \approx suc y$
23	22	ex	$⊢ y \in ω \to (y \approx y \to suc y \approx suc y)$
24	2 4 6 8 11 23	finds	$⊢ A \in ω \to A \approx A$

Metamath Proof Explorer

Theorem enrefnn

Proof