Metamath Proof Explorer


Theorem lcfls1N

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

Ref Expression
Hypotheses lcfls1.c 𝐶 = { 𝑓𝐹 ∣ ( ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 ) }
lcfls1.g ( 𝜑𝐺𝐹 )
Assertion lcfls1N ( 𝜑 → ( 𝐺𝐶 ↔ ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 lcfls1.c 𝐶 = { 𝑓𝐹 ∣ ( ( ‘ ( ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( ‘ ( 𝐿𝑓 ) ) ⊆ 𝑄 ) }
2 lcfls1.g ( 𝜑𝐺𝐹 )
3 1 lcfls1lem ( 𝐺𝐶 ↔ ( 𝐺𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) )
4 3anass ( ( 𝐺𝐹 ∧ ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ↔ ( 𝐺𝐹 ∧ ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ) )
5 3 4 bitri ( 𝐺𝐶 ↔ ( 𝐺𝐹 ∧ ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ) )
6 2 biantrurd ( 𝜑 → ( ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ↔ ( 𝐺𝐹 ∧ ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ) ) )
7 5 6 bitr4id ( 𝜑 → ( 𝐺𝐶 ↔ ( ( ‘ ( ‘ ( 𝐿𝐺 ) ) ) = ( 𝐿𝐺 ) ∧ ( ‘ ( 𝐿𝐺 ) ) ⊆ 𝑄 ) ) )