Theorem hfpw

Description: The power class of an HF set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015)

	Ref	Expression
Assertion	hfpw	|- ( A e. Hf -> ~P A e. Hf )

Proof

Step	Hyp	Ref	Expression
1		rankpwg	|- ( A e. Hf -> ( rank ` ~P A ) = suc ( rank ` A ) )
2		elhf2g	|- ( A e. Hf -> ( A e. Hf <-> ( rank ` A ) e. _om ) )
3	2	ibi	|- ( A e. Hf -> ( rank ` A ) e. _om )
4		peano2	|- ( ( rank ` A ) e. _om -> suc ( rank ` A ) e. _om )
5	3 4	syl	|- ( A e. Hf -> suc ( rank ` A ) e. _om )
6	1 5	eqeltrd	|- ( A e. Hf -> ( rank ` ~P A ) e. _om )
7		pwexg	|- ( A e. Hf -> ~P A e. _V )
8		elhf2g	|- ( ~P A e. _V -> ( ~P A e. Hf <-> ( rank ` ~P A ) e. _om ) )
9	7 8	syl	|- ( A e. Hf -> ( ~P A e. Hf <-> ( rank ` ~P A ) e. _om ) )
10	6 9	mpbird	|- ( A e. Hf -> ~P A e. Hf )