Theorem elhf3OLD

Description: Obsolete version of elhf3 as of 17-Sep-2026. (Contributed by Eric Schmidt, 8-Sep-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elhf3OLD	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) )

Proof

Step	Hyp	Ref	Expression
1		hffi	⊢ ( 𝐴 ∈ HF → 𝐴 ∈ Fin )
2		hfelhf	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ HF ) → 𝑥 ∈ HF )
3	2	expcom	⊢ ( 𝐴 ∈ HF → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ HF ) )
4	3	ssrdv	⊢ ( 𝐴 ∈ HF → 𝐴 ⊆ HF )
5	1 4	jca	⊢ ( 𝐴 ∈ HF → ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) )
6		eleq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ HF ↔ ∅ ∈ HF ) )
7		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ HF ↔ 𝑦 ∈ HF ) )
8		eleq1	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ∈ HF ↔ ( 𝑦 ∪ { 𝑧 } ) ∈ HF ) )
9		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ HF ↔ 𝐴 ∈ HF ) )
10		0hf	⊢ ∅ ∈ HF
11	10	a1i	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) → ∅ ∈ HF )
12		eldifi	⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → 𝑧 ∈ 𝐴 )
13		ssel2	⊢ ( ( 𝐴 ⊆ HF ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ HF )
14	12 13	sylan2	⊢ ( ( 𝐴 ⊆ HF ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑧 ∈ HF )
15		hfadj	⊢ ( ( 𝑦 ∈ HF ∧ 𝑧 ∈ HF ) → ( 𝑦 ∪ { 𝑧 } ) ∈ HF )
16	15	expcom	⊢ ( 𝑧 ∈ HF → ( 𝑦 ∈ HF → ( 𝑦 ∪ { 𝑧 } ) ∈ HF ) )
17	14 16	syl	⊢ ( ( 𝐴 ⊆ HF ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑦 ∈ HF → ( 𝑦 ∪ { 𝑧 } ) ∈ HF ) )
18	17	ad2ant2l	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑦 ∈ HF → ( 𝑦 ∪ { 𝑧 } ) ∈ HF ) )
19		simpl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) → 𝐴 ∈ Fin )
20	6 7 8 9 11 18 19	findcard2d	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) → 𝐴 ∈ HF )
21	5 20	impbii	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) )