Metamath Proof Explorer

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 Could not format assertion : No typesetting found for |- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) ) with typecode |-

Proof

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