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	|- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) )

Proof

Step	Hyp	Ref	Expression
1		hffi	|- ( A e. HF -> A e. Fin )
2		hfelhf	|- ( ( x e. A /\ A e. HF ) -> x e. HF )
3	2	expcom	|- ( A e. HF -> ( x e. A -> x e. HF ) )
4	3	ssrdv	|- ( A e. HF -> A C_ HF )
5	1 4	jca	|- ( A e. HF -> ( A e. Fin /\ A C_ HF ) )
6		eleq1	|- ( x = (/) -> ( x e. HF <-> (/) e. HF ) )
7		eleq1	|- ( x = y -> ( x e. HF <-> y e. HF ) )
8		eleq1	|- ( x = ( y u. { z } ) -> ( x e. HF <-> ( y u. { z } ) e. HF ) )
9		eleq1	|- ( x = A -> ( x e. HF <-> A e. HF ) )
10		0hf	|- (/) e. HF
11	10	a1i	|- ( ( A e. Fin /\ A C_ HF ) -> (/) e. HF )
12		eldifi	|- ( z e. ( A \ y ) -> z e. A )
13		ssel2	|- ( ( A C_ HF /\ z e. A ) -> z e. HF )
14	12 13	sylan2	|- ( ( A C_ HF /\ z e. ( A \ y ) ) -> z e. HF )
15		hfadj	|- ( ( y e. HF /\ z e. HF ) -> ( y u. { z } ) e. HF )
16	15	expcom	|- ( z e. HF -> ( y e. HF -> ( y u. { z } ) e. HF ) )
17	14 16	syl	|- ( ( A C_ HF /\ z e. ( A \ y ) ) -> ( y e. HF -> ( y u. { z } ) e. HF ) )
18	17	ad2ant2l	|- ( ( ( A e. Fin /\ A C_ HF ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( y e. HF -> ( y u. { z } ) e. HF ) )
19		simpl	|- ( ( A e. Fin /\ A C_ HF ) -> A e. Fin )
20	6 7 8 9 11 18 19	findcard2d	|- ( ( A e. Fin /\ A C_ HF ) -> A e. HF )
21	5 20	impbii	|- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) )