Theorem hfpwOLD

Description: Obsolete version of hfpw as of 17-Sep-2026. (Contributed by Scott Fenton, 16-Jul-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hfpwOLD	|- ( 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 )