Theorem lcfl1lem 42127

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

Hypothesis

Ref	Expression
lcfl1.c	⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}

Assertion

Ref	Expression
lcfl1lem	⊢ (𝐺 ∈ 𝐶 ↔ (𝐺 ∈ 𝐹 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)))

Distinct variable groups:   𝑓,𝐹   𝑓,𝐺   𝑓,𝐿   ⊥ ,𝑓

Allowed substitution hint:   𝐶(𝑓)

Proof of Theorem lcfl1lem

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {crab 3417  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533

This theorem is referenced by:  lcfl1  42128  lcfl8b  42140  lclkrlem1  42142  lclkrlem2  42168  lclkr  42169  lcfls1c  42172  lcfrlem9  42186  mapdvalc  42265  mapdval2N  42266  mapdval4N  42268  mapdordlem1a  42270  mapdordlem1bN  42271  mapdrvallem2  42281