Theorem elhf2

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

	Ref	Expression
Hypothesis	elhf2.1	⊢ 𝐴 ∈ V
Assertion	elhf2	⊢ ( 𝐴 ∈ HF ↔ ( rank ‘ 𝐴 ) ∈ ω )

Proof

Step	Hyp	Ref	Expression
1		elhf2.1	⊢ 𝐴 ∈ V
2		elhf	⊢ ( 𝐴 ∈ HF ↔ ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )
3		omon	⊢ ( ω ∈ On ∨ ω = On )
4		nnon	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On )
5	1	rankr1a	⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝑥 ) )
6	4 5	syl	⊢ ( 𝑥 ∈ ω → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝑥 ) )
7	6	adantl	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ ω ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝑥 ) )
8		elnn	⊢ ( ( ( rank ‘ 𝐴 ) ∈ 𝑥 ∧ 𝑥 ∈ ω ) → ( rank ‘ 𝐴 ) ∈ ω )
9	8	expcom	⊢ ( 𝑥 ∈ ω → ( ( rank ‘ 𝐴 ) ∈ 𝑥 → ( rank ‘ 𝐴 ) ∈ ω ) )
10	9	adantl	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ ω ) → ( ( rank ‘ 𝐴 ) ∈ 𝑥 → ( rank ‘ 𝐴 ) ∈ ω ) )
11	7 10	sylbid	⊢ ( ( ω ∈ On ∧ 𝑥 ∈ ω ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → ( rank ‘ 𝐴 ) ∈ ω ) )
12	11	rexlimdva	⊢ ( ω ∈ On → ( ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) → ( rank ‘ 𝐴 ) ∈ ω ) )
13		peano2	⊢ ( ( rank ‘ 𝐴 ) ∈ ω → suc ( rank ‘ 𝐴 ) ∈ ω )
14	13	adantr	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ω ∈ On ) → suc ( rank ‘ 𝐴 ) ∈ ω )
15		r1rankid	⊢ ( 𝐴 ∈ V → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
16	1 15	mp1i	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ω ∈ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
17	1	elpw	⊢ ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
18	16 17	sylibr	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ω ∈ On ) → 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
19		nnon	⊢ ( ( rank ‘ 𝐴 ) ∈ ω → ( rank ‘ 𝐴 ) ∈ On )
20		r1suc	⊢ ( ( rank ‘ 𝐴 ) ∈ On → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
21	19 20	syl	⊢ ( ( rank ‘ 𝐴 ) ∈ ω → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
22	21	adantr	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ω ∈ On ) → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
23	18 22	eleqtrrd	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ω ∈ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
24		fveq2	⊢ ( 𝑥 = suc ( rank ‘ 𝐴 ) → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
25	24	eleq2d	⊢ ( 𝑥 = suc ( rank ‘ 𝐴 ) → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ) )
26	25	rspcev	⊢ ( ( suc ( rank ‘ 𝐴 ) ∈ ω ∧ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ) → ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )
27	14 23 26	syl2anc	⊢ ( ( ( rank ‘ 𝐴 ) ∈ ω ∧ ω ∈ On ) → ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) )
28	27	expcom	⊢ ( ω ∈ On → ( ( rank ‘ 𝐴 ) ∈ ω → ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
29	12 28	impbid	⊢ ( ω ∈ On → ( ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
30	1	tz9.13	⊢ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 )
31		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
32	30 31	2th	⊢ ( ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ On )
33		rexeq	⊢ ( ω = On → ( ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ) )
34		eleq2	⊢ ( ω = On → ( ( rank ‘ 𝐴 ) ∈ ω ↔ ( rank ‘ 𝐴 ) ∈ On ) )
35	33 34	bibi12d	⊢ ( ω = On → ( ( ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ ω ) ↔ ( ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ On ) ) )
36	32 35	mpbiri	⊢ ( ω = On → ( ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
37	29 36	jaoi	⊢ ( ( ω ∈ On ∨ ω = On ) → ( ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ ω ) )
38	3 37	ax-mp	⊢ ( ∃ 𝑥 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ∈ ω )
39	2 38	bitri	⊢ ( 𝐴 ∈ HF ↔ ( rank ‘ 𝐴 ) ∈ ω )