Metamath Proof Explorer

Theorem lcfls1c

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

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

Proof

Step Hyp Ref Expression
1 lcfls1.c ⊢C=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f∧⊥˙⁡L⁡f⊆Q
2 lcfls1c.c ⊢D=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
3 df-3an ⊢G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q↔G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q
4 1 lcfls1lem ⊢G∈C↔G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q
5 2 lcfl1lem ⊢G∈D↔G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G
6 5 anbi1i ⊢G∈D∧⊥˙⁡L⁡G⊆Q↔G∈F∧⊥˙⁡⊥˙⁡L⁡G=L⁡G∧⊥˙⁡L⁡G⊆Q
7 3 4 6 3bitr4i ⊢G∈C↔G∈D∧⊥˙⁡L⁡G⊆Q