Metamath Proof Explorer

Theorem lcfls1lem

Description: Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypothesis lcfls1.c ⊢C=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f∧⊥˙⁡L⁡f⊆Q
Assertion lcfls1lem ⊢G∈C↔G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q

Proof

Step Hyp Ref Expression
1 lcfls1.c ⊢C=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f∧⊥˙⁡L⁡f⊆Q
2 fveq2 ⊢f=G→L⁡f=L⁡G
3 2 fveq2d ⊢f=G→⊥˙⁡L⁡f=⊥˙⁡L⁡G
4 3 fveq2d ⊢f=G→⊥˙⁡⊥˙⁡L⁡f=⊥˙⁡⊥˙⁡L⁡G
5 4 2 eqeq12d ⊢f=G→⊥˙⁡⊥˙⁡L⁡f=L⁡f↔⊥˙⁡⊥˙⁡L⁡G=L⁡G
6 3 sseq1d ⊢f=G→⊥˙⁡L⁡f⊆Q↔⊥˙⁡L⁡G⊆Q
7 5 6 anbi12d ⊢f=G→⊥˙⁡⊥˙⁡L⁡f=L⁡f∧⊥˙⁡L⁡f⊆Q↔⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q
8 7 1 elrab2 ⊢G∈C↔G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q
9 3anass ⊢G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q↔G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q
10 8 9 bitr4i ⊢G∈C↔G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q