Theorem elhf2

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

	Ref	Expression
Hypothesis	elhf2.1	|- A e. _V
Assertion	elhf2	|- ( A e. Hf <-> ( rank ` A ) e. _om )

Proof

Step	Hyp	Ref	Expression
1		elhf2.1	|- A e. _V
2		elhf	|- ( A e. Hf <-> E. x e. _om A e. ( R1 ` x ) )
3		omon	|- ( _om e. On \/ _om = On )
4		nnon	|- ( x e. _om -> x e. On )
5	1	rankr1a	|- ( x e. On -> ( A e. ( R1 ` x ) <-> ( rank ` A ) e. x ) )
6	4 5	syl	|- ( x e. _om -> ( A e. ( R1 ` x ) <-> ( rank ` A ) e. x ) )
7	6	adantl	|- ( ( _om e. On /\ x e. _om ) -> ( A e. ( R1 ` x ) <-> ( rank ` A ) e. x ) )
8		elnn	|- ( ( ( rank ` A ) e. x /\ x e. _om ) -> ( rank ` A ) e. _om )
9	8	expcom	|- ( x e. _om -> ( ( rank ` A ) e. x -> ( rank ` A ) e. _om ) )
10	9	adantl	|- ( ( _om e. On /\ x e. _om ) -> ( ( rank ` A ) e. x -> ( rank ` A ) e. _om ) )
11	7 10	sylbid	|- ( ( _om e. On /\ x e. _om ) -> ( A e. ( R1 ` x ) -> ( rank ` A ) e. _om ) )
12	11	rexlimdva	|- ( _om e. On -> ( E. x e. _om A e. ( R1 ` x ) -> ( rank ` A ) e. _om ) )
13		peano2	|- ( ( rank ` A ) e. _om -> suc ( rank ` A ) e. _om )
14	13	adantr	|- ( ( ( rank ` A ) e. _om /\ _om e. On ) -> suc ( rank ` A ) e. _om )
15		r1rankid	|- ( A e. _V -> A C_ ( R1 ` ( rank ` A ) ) )
16	1 15	mp1i	|- ( ( ( rank ` A ) e. _om /\ _om e. On ) -> A C_ ( R1 ` ( rank ` A ) ) )
17	1	elpw	|- ( A e. ~P ( R1 ` ( rank ` A ) ) <-> A C_ ( R1 ` ( rank ` A ) ) )
18	16 17	sylibr	|- ( ( ( rank ` A ) e. _om /\ _om e. On ) -> A e. ~P ( R1 ` ( rank ` A ) ) )
19		nnon	|- ( ( rank ` A ) e. _om -> ( rank ` A ) e. On )
20		r1suc	|- ( ( rank ` A ) e. On -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) )
21	19 20	syl	|- ( ( rank ` A ) e. _om -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) )
22	21	adantr	|- ( ( ( rank ` A ) e. _om /\ _om e. On ) -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) )
23	18 22	eleqtrrd	|- ( ( ( rank ` A ) e. _om /\ _om e. On ) -> A e. ( R1 ` suc ( rank ` A ) ) )
24		fveq2	|- ( x = suc ( rank ` A ) -> ( R1 ` x ) = ( R1 ` suc ( rank ` A ) ) )
25	24	eleq2d	|- ( x = suc ( rank ` A ) -> ( A e. ( R1 ` x ) <-> A e. ( R1 ` suc ( rank ` A ) ) ) )
26	25	rspcev	|- ( ( suc ( rank ` A ) e. _om /\ A e. ( R1 ` suc ( rank ` A ) ) ) -> E. x e. _om A e. ( R1 ` x ) )
27	14 23 26	syl2anc	|- ( ( ( rank ` A ) e. _om /\ _om e. On ) -> E. x e. _om A e. ( R1 ` x ) )
28	27	expcom	|- ( _om e. On -> ( ( rank ` A ) e. _om -> E. x e. _om A e. ( R1 ` x ) ) )
29	12 28	impbid	|- ( _om e. On -> ( E. x e. _om A e. ( R1 ` x ) <-> ( rank ` A ) e. _om ) )
30	1	tz9.13	|- E. x e. On A e. ( R1 ` x )
31		rankon	|- ( rank ` A ) e. On
32	30 31	2th	|- ( E. x e. On A e. ( R1 ` x ) <-> ( rank ` A ) e. On )
33		rexeq	|- ( _om = On -> ( E. x e. _om A e. ( R1 ` x ) <-> E. x e. On A e. ( R1 ` x ) ) )
34		eleq2	|- ( _om = On -> ( ( rank ` A ) e. _om <-> ( rank ` A ) e. On ) )
35	33 34	bibi12d	|- ( _om = On -> ( ( E. x e. _om A e. ( R1 ` x ) <-> ( rank ` A ) e. _om ) <-> ( E. x e. On A e. ( R1 ` x ) <-> ( rank ` A ) e. On ) ) )
36	32 35	mpbiri	|- ( _om = On -> ( E. x e. _om A e. ( R1 ` x ) <-> ( rank ` A ) e. _om ) )
37	29 36	jaoi	|- ( ( _om e. On \/ _om = On ) -> ( E. x e. _om A e. ( R1 ` x ) <-> ( rank ` A ) e. _om ) )
38	3 37	ax-mp	|- ( E. x e. _om A e. ( R1 ` x ) <-> ( rank ` A ) e. _om )
39	2 38	bitri	|- ( A e. Hf <-> ( rank ` A ) e. _om )