Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lcfl1 Structured version   Visualization version   GIF version

Theorem lcfl1 37317
Description: Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.)
Hypotheses
Ref Expression
lcfl1.c 𝐶 = {𝑓𝐹 ∣ ( ‘( ‘(𝐿𝑓))) = (𝐿𝑓)}
lcfl1.g (𝜑𝐺𝐹)
Assertion
Ref Expression
lcfl1 (𝜑 → (𝐺𝐶 ↔ ( ‘( ‘(𝐿𝐺))) = (𝐿𝐺)))
Distinct variable groups:   𝑓,𝐹   𝑓,𝐺   𝑓,𝐿   ,𝑓
Allowed substitution hints:   𝜑(𝑓)   𝐶(𝑓)

Proof of Theorem lcfl1
StepHypRef Expression
1 lcfl1.g . . 3 (𝜑𝐺𝐹)
21biantrurd 523 . 2 (𝜑 → (( ‘( ‘(𝐿𝐺))) = (𝐿𝐺) ↔ (𝐺𝐹 ∧ ( ‘( ‘(𝐿𝐺))) = (𝐿𝐺))))
3 lcfl1.c . . 3 𝐶 = {𝑓𝐹 ∣ ( ‘( ‘(𝐿𝑓))) = (𝐿𝑓)}
43lcfl1lem 37316 . 2 (𝐺𝐶 ↔ (𝐺𝐹 ∧ ( ‘( ‘(𝐿𝐺))) = (𝐿𝐺)))
52, 4syl6rbbr 280 1 (𝜑 → (𝐺𝐶 ↔ ( ‘( ‘(𝐿𝐺))) = (𝐿𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383   = wceq 1634  wcel 2148  {crab 3068  cfv 6042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rex 3070  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-iota 6005  df-fv 6050
This theorem is referenced by:  lcfl2  37318  lcfl5  37321  lcfl5a  37322  lcfl6  37325  lcfl8  37327  lcfl8a  37328  lclkrlem2  37357
  Copyright terms: Public domain W3C validator