Metamath Proof Explorer


Theorem lcfl1lem

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

Ref Expression
Hypothesis lcfl1.c 𝐶 = { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
Assertion lcfl1lem ( 𝐺𝐶 ↔ ( 𝐺𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 lcfl1.c 𝐶 = { 𝑓𝐹 ∣ ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) }
2 fveq2 ( 𝑓 = 𝐺 → ( 𝐿𝑓 ) = ( 𝐿𝐺 ) )
3 2 fveq2d ( 𝑓 = 𝐺 → ( ‘ ( 𝐿𝑓 ) ) = ( ‘ ( 𝐿𝐺 ) ) )
4 3 fveq2d ( 𝑓 = 𝐺 → ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) )
5 4 2 eqeq12d ( 𝑓 = 𝐺 → ( ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ↔ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ) )
6 5 1 elrab2 ( 𝐺𝐶 ↔ ( 𝐺𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ) )