elhf2

Description: Alternate form of membership in the hereditarily finite sets. (Contributed by Scott Fenton, 13-Jul-2015)

		Ref	Expression
	Hypothesis	elhf2.1	$⊢ A \in V$
	Assertion	elhf2	$⊢ A \in Hf \leftrightarrow rank (A) \in ω$

Proof

Step	Hyp	Ref	Expression
1		elhf2.1	$⊢ A \in V$
2		elhf	$⊢ A \in Hf \leftrightarrow \exists x \in ω A \in R_{1} (x)$
3		omon	$⊢ (ω \in On \lor ω = On)$
4		nnon	$⊢ x \in ω \to x \in On$
5	1	rankr1a	$⊢ x \in On \to (A \in R_{1} (x) \leftrightarrow rank (A) \in x)$
6	4 5	syl	$⊢ x \in ω \to (A \in R_{1} (x) \leftrightarrow rank (A) \in x)$
7	6	adantl	$⊢ (ω \in On \land x \in ω) \to (A \in R_{1} (x) \leftrightarrow rank (A) \in x)$
8		elnn	$⊢ (rank (A) \in x \land x \in ω) \to rank (A) \in ω$
9	8	expcom	$⊢ x \in ω \to (rank (A) \in x \to rank (A) \in ω)$
10	9	adantl	$⊢ (ω \in On \land x \in ω) \to (rank (A) \in x \to rank (A) \in ω)$
11	7 10	sylbid	$⊢ (ω \in On \land x \in ω) \to (A \in R_{1} (x) \to rank (A) \in ω)$
12	11	rexlimdva	$⊢ ω \in On \to (\exists x \in ω A \in R_{1} (x) \to rank (A) \in ω)$
13		peano2	$⊢ rank (A) \in ω \to suc rank (A) \in ω$
14	13	adantr	$⊢ (rank (A) \in ω \land ω \in On) \to suc rank (A) \in ω$
15		r1rankid	$⊢ A \in V \to A \subseteq R_{1} (rank (A))$
16	1 15	mp1i	$⊢ (rank (A) \in ω \land ω \in On) \to A \subseteq R_{1} (rank (A))$
17	1	elpw	$⊢ A \in 𝒫 R_{1} (rank (A)) \leftrightarrow A \subseteq R_{1} (rank (A))$
18	16 17	sylibr	$⊢ (rank (A) \in ω \land ω \in On) \to A \in 𝒫 R_{1} (rank (A))$
19		nnon	$⊢ rank (A) \in ω \to rank (A) \in On$
20		r1suc	$⊢ rank (A) \in On \to R_{1} (suc rank (A)) = 𝒫 R_{1} (rank (A))$
21	19 20	syl	$⊢ rank (A) \in ω \to R_{1} (suc rank (A)) = 𝒫 R_{1} (rank (A))$
22	21	adantr	$⊢ (rank (A) \in ω \land ω \in On) \to R_{1} (suc rank (A)) = 𝒫 R_{1} (rank (A))$
23	18 22	eleqtrrd	$⊢ (rank (A) \in ω \land ω \in On) \to A \in R_{1} (suc rank (A))$
24		fveq2	$⊢ x = suc rank (A) \to R_{1} (x) = R_{1} (suc rank (A))$
25	24	eleq2d	$⊢ x = suc rank (A) \to (A \in R_{1} (x) \leftrightarrow A \in R_{1} (suc rank (A)))$
26	25	rspcev	$⊢ (suc rank (A) \in ω \land A \in R_{1} (suc rank (A))) \to \exists x \in ω A \in R_{1} (x)$
27	14 23 26	syl2anc	$⊢ (rank (A) \in ω \land ω \in On) \to \exists x \in ω A \in R_{1} (x)$
28	27	expcom	$⊢ ω \in On \to (rank (A) \in ω \to \exists x \in ω A \in R_{1} (x))$
29	12 28	impbid	$⊢ ω \in On \to (\exists x \in ω A \in R_{1} (x) \leftrightarrow rank (A) \in ω)$
30	1	tz9.13	$⊢ \exists x \in On A \in R_{1} (x)$
31		rankon	$⊢ rank (A) \in On$
32	30 31	2th	$⊢ \exists x \in On A \in R_{1} (x) \leftrightarrow rank (A) \in On$
33		rexeq	$⊢ ω = On \to (\exists x \in ω A \in R_{1} (x) \leftrightarrow \exists x \in On A \in R_{1} (x))$
34		eleq2	$⊢ ω = On \to (rank (A) \in ω \leftrightarrow rank (A) \in On)$
35	33 34	bibi12d	$⊢ ω = On \to ((\exists x \in ω A \in R_{1} (x) \leftrightarrow rank (A) \in ω) \leftrightarrow (\exists x \in On A \in R_{1} (x) \leftrightarrow rank (A) \in On))$
36	32 35	mpbiri	$⊢ ω = On \to (\exists x \in ω A \in R_{1} (x) \leftrightarrow rank (A) \in ω)$
37	29 36	jaoi	$⊢ (ω \in On \lor ω = On) \to (\exists x \in ω A \in R_{1} (x) \leftrightarrow rank (A) \in ω)$
38	3 37	ax-mp	$⊢ \exists x \in ω A \in R_{1} (x) \leftrightarrow rank (A) \in ω$
39	2 38	bitri	$⊢ A \in Hf \leftrightarrow rank (A) \in ω$

Metamath Proof Explorer

Theorem elhf2

Proof