Metamath Proof Explorer

Theorem lcfl1

Description: Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014)

Ref Expression
Hypotheses lcfl1.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
lcfl1.g ⊢ φ → G ∈ F
Assertion lcfl1 ⊢ φ → G ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G

Proof

Step Hyp Ref Expression
1 lcfl1.c ⊢ C = f ∈ F | ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ f = L ⁡ f
2 lcfl1.g ⊢ φ → G ∈ F
3 1 lcfl1lem ⊢ G ∈ C ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
4 2 biantrurd ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G ↔ G ∈ F ∧ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G
5 3 4 bitr4id ⊢ φ → G ∈ C ↔ ⊥ ˙ ⁡ ⊥ ˙ ⁡ L ⁡ G = L ⁡ G