hfelhf

Description: Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015)

		Ref	Expression
	Assertion	hfelhf	$⊢ (A \in B \land B \in Hf) \to A \in Hf$

Step	Hyp	Ref	Expression
1		rankelg	$⊢ (B \in Hf \land A \in B) \to rank (A) \in rank (B)$
2	1	ancoms	$⊢ (A \in B \land B \in Hf) \to rank (A) \in rank (B)$
3		elhf2g	$⊢ B \in Hf \to (B \in Hf \leftrightarrow rank (B) \in ω)$
4	3	ibi	$⊢ B \in Hf \to rank (B) \in ω$
5		elnn	$⊢ (rank (A) \in rank (B) \land rank (B) \in ω) \to rank (A) \in ω$
6		elhf2g	$⊢ A \in B \to (A \in Hf \leftrightarrow rank (A) \in ω)$
7	5 6	syl5ibr	$⊢ A \in B \to ((rank (A) \in rank (B) \land rank (B) \in ω) \to A \in Hf)$
8	7	expcomd	$⊢ A \in B \to (rank (B) \in ω \to (rank (A) \in rank (B) \to A \in Hf))$
9	8	imp	$⊢ (A \in B \land rank (B) \in ω) \to (rank (A) \in rank (B) \to A \in Hf)$
10	4 9	sylan2	$⊢ (A \in B \land B \in Hf) \to (rank (A) \in rank (B) \to A \in Hf)$
11	2 10	mpd	$⊢ (A \in B \land B \in Hf) \to A \in Hf$

Metamath Proof Explorer