HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  cbvf GIF version

Theorem cbvf 179
Description: Change bound variables in a lambda abstraction. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
cbvf.1 A:β
cbvf.2 ⊤⊧[(λy:α Az:α) = A]
cbvf.3 ⊤⊧[(λx:α Bz:α) = B]
cbvf.4 [x:α = y:α]⊧[A = B]
Assertion
Ref Expression
cbvf ⊤⊧[λx:α A = λy:α B]
Distinct variable groups:   z,A   z,B   x,y,z,α

Proof of Theorem cbvf
Dummy variable p is distinct from all other variables.
StepHypRef Expression
1 cbvf.1 . . . . 5 A:β
21wl 66 . . . 4 λx:α A:(αβ)
3 wv 64 . . . 4 p:α:α
42, 3wc 50 . . 3 (λx:α Ap:α):β
54wl 66 . 2 λp:α (λx:α Ap:α):(αβ)
6 cbvf.4 . . . . . . . 8 [x:α = y:α]⊧[A = B]
71, 6eqtypi 78 . . . . . . 7 B:β
87wl 66 . . . . . 6 λy:α B:(αβ)
98, 3wc 50 . . . . 5 (λy:α Bp:α):β
104, 9weqi 76 . . . 4 [(λx:α Ap:α) = (λy:α Bp:α)]:∗
11 wv 64 . . . . 5 y:α:α
12 cbvf.3 . . . . 5 ⊤⊧[(λx:α Bz:α) = B]
13 wv 64 . . . . . 6 z:α:α
1411, 13ax-17 105 . . . . 5 ⊤⊧[(λx:α y:αz:α) = y:α]
151, 11, 6, 12, 14clf 115 . . . 4 ⊤⊧[(λx:α Ay:α) = B]
16 weq 41 . . . . 5 = :(β → (β → ∗))
1716, 13ax-17 105 . . . . 5 ⊤⊧[(λy:α = z:α) = = ]
18 cbvf.2 . . . . . . 7 ⊤⊧[(λy:α Az:α) = A]
191, 13, 18hbl 112 . . . . . 6 ⊤⊧[(λy:α λx:α Az:α) = λx:α A]
203, 13ax-17 105 . . . . . 6 ⊤⊧[(λy:α p:αz:α) = p:α]
212, 3, 13, 19, 20hbc 110 . . . . 5 ⊤⊧[(λy:α (λx:α Ap:α)z:α) = (λx:α Ap:α)]
2218ax-cb1 29 . . . . . . 7 ⊤:∗
237, 13, 22hbl1 104 . . . . . 6 ⊤⊧[(λy:α λy:α Bz:α) = λy:α B]
248, 3, 13, 23, 20hbc 110 . . . . 5 ⊤⊧[(λy:α (λy:α Bp:α)z:α) = (λy:α Bp:α)]
2516, 4, 13, 9, 17, 21, 24hbov 111 . . . 4 ⊤⊧[(λy:α [(λx:α Ap:α) = (λy:α Bp:α)]z:α) = [(λx:α Ap:α) = (λy:α Bp:α)]]
262, 11wc 50 . . . . 5 (λx:α Ay:α):β
2711, 3weqi 76 . . . . . . 7 [y:α = p:α]:∗
2827id 25 . . . . . 6 [y:α = p:α]⊧[y:α = p:α]
292, 11, 28ceq2 90 . . . . 5 [y:α = p:α]⊧[(λx:α Ay:α) = (λx:α Ap:α)]
3029ax-cb1 29 . . . . . . 7 [y:α = p:α]:∗
318, 11wc 50 . . . . . . . 8 (λy:α By:α):β
327beta 92 . . . . . . . 8 ⊤⊧[(λy:α By:α) = B]
3331, 32eqcomi 79 . . . . . . 7 ⊤⊧[B = (λy:α By:α)]
3430, 33a1i 28 . . . . . 6 [y:α = p:α]⊧[B = (λy:α By:α)]
358, 11, 28ceq2 90 . . . . . 6 [y:α = p:α]⊧[(λy:α By:α) = (λy:α Bp:α)]
367, 34, 35eqtri 95 . . . . 5 [y:α = p:α]⊧[B = (λy:α Bp:α)]
3716, 26, 7, 29, 36oveq12 100 . . . 4 [y:α = p:α]⊧[[(λx:α Ay:α) = B] = [(λx:α Ap:α) = (λy:α Bp:α)]]
383, 10, 15, 25, 37insti 114 . . 3 ⊤⊧[(λx:α Ap:α) = (λy:α Bp:α)]
394, 38leq 91 . 2 ⊤⊧[λp:α (λx:α Ap:α) = λp:α (λy:α Bp:α)]
402eta 178 . 2 ⊤⊧[λp:α (λx:α Ap:α) = λx:α A]
418eta 178 . 2 ⊤⊧[λp:α (λy:α Bp:α) = λy:α B]
425, 39, 40, 413eqtr3i 97 1 ⊤⊧[λx:α A = λy:α B]
Colors of variables: type var term
Syntax hints:  tv 1  ht 2  hb 3  kc 5  λkl 6   = ke 7  kt 8  [kbr 9  wffMMJ2 11  wffMMJ2t 12
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-wctl 31  ax-wctr 32  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wct 47  ax-wc 49  ax-ceq 51  ax-wv 63  ax-wl 65  ax-beta 67  ax-distrc 68  ax-leq 69  ax-distrl 70  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80  ax-hbl1 103  ax-17 105  ax-inst 113  ax-eta 177
This theorem depends on definitions:  df-ov 73  df-al 126
This theorem is referenced by:  cbv  180
  Copyright terms: Public domain W3C validator