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.

Step	Hyp	Ref	Expression
1		cbvf.1	. . . . 5 ⊢ A:β
2	1	wl 66	. . . 4 ⊢ λx:α A:(α → β)
3		wv 64	. . . 4 ⊢ p:α:α
4	2, 3	wc 50	. . 3 ⊢ (λx:α Ap:α):β
5	4	wl 66	. 2 ⊢ λp:α (λx:α Ap:α):(α → β)
6		cbvf.4	. . . . . . . 8 ⊢ [x:α = y:α]⊧[A = B]
7	1, 6	eqtypi 78	. . . . . . 7 ⊢ B:β
8	7	wl 66	. . . . . 6 ⊢ λy:α B:(α → β)
9	8, 3	wc 50	. . . . 5 ⊢ (λy:α Bp:α):β
10	4, 9	weqi 76	. . . 4 ⊢ [(λx:α Ap:α) = (λy:α Bp:α)]:∗
11		wv 64	. . . . 5 ⊢ y:α:α
12		cbvf.3	. . . . 5 ⊢ ⊤⊧[(λx:α Bz:α) = B]
13		wv 64	. . . . . 6 ⊢ z:α:α
14	11, 13	ax-17 105	. . . . 5 ⊢ ⊤⊧[(λx:α y:αz:α) = y:α]
15	1, 11, 6, 12, 14	clf 115	. . . 4 ⊢ ⊤⊧[(λx:α Ay:α) = B]
16		weq 41	. . . . 5 ⊢ = :(β → (β → ∗))
17	16, 13	ax-17 105	. . . . 5 ⊢ ⊤⊧[(λy:α = z:α) = = ]
18		cbvf.2	. . . . . . 7 ⊢ ⊤⊧[(λy:α Az:α) = A]
19	1, 13, 18	hbl 112	. . . . . 6 ⊢ ⊤⊧[(λy:α λx:α Az:α) = λx:α A]
20	3, 13	ax-17 105	. . . . . 6 ⊢ ⊤⊧[(λy:α p:αz:α) = p:α]
21	2, 3, 13, 19, 20	hbc 110	. . . . 5 ⊢ ⊤⊧[(λy:α (λx:α Ap:α)z:α) = (λx:α Ap:α)]
22	18	ax-cb1 29	. . . . . . 7 ⊢ ⊤:∗
23	7, 13, 22	hbl1 104	. . . . . 6 ⊢ ⊤⊧[(λy:α λy:α Bz:α) = λy:α B]
24	8, 3, 13, 23, 20	hbc 110	. . . . 5 ⊢ ⊤⊧[(λy:α (λy:α Bp:α)z:α) = (λy:α Bp:α)]
25	16, 4, 13, 9, 17, 21, 24	hbov 111	. . . 4 ⊢ ⊤⊧[(λy:α [(λx:α Ap:α) = (λy:α Bp:α)]z:α) = [(λx:α Ap:α) = (λy:α Bp:α)]]
26	2, 11	wc 50	. . . . 5 ⊢ (λx:α Ay:α):β
27	11, 3	weqi 76	. . . . . . 7 ⊢ [y:α = p:α]:∗
28	27	id 25	. . . . . 6 ⊢ [y:α = p:α]⊧[y:α = p:α]
29	2, 11, 28	ceq2 90	. . . . 5 ⊢ [y:α = p:α]⊧[(λx:α Ay:α) = (λx:α Ap:α)]
30	29	ax-cb1 29	. . . . . . 7 ⊢ [y:α = p:α]:∗
31	8, 11	wc 50	. . . . . . . 8 ⊢ (λy:α By:α):β
32	7	beta 92	. . . . . . . 8 ⊢ ⊤⊧[(λy:α By:α) = B]
33	31, 32	eqcomi 79	. . . . . . 7 ⊢ ⊤⊧[B = (λy:α By:α)]
34	30, 33	a1i 28	. . . . . 6 ⊢ [y:α = p:α]⊧[B = (λy:α By:α)]
35	8, 11, 28	ceq2 90	. . . . . 6 ⊢ [y:α = p:α]⊧[(λy:α By:α) = (λy:α Bp:α)]
36	7, 34, 35	eqtri 95	. . . . 5 ⊢ [y:α = p:α]⊧[B = (λy:α Bp:α)]
37	16, 26, 7, 29, 36	oveq12 100	. . . 4 ⊢ [y:α = p:α]⊧[[(λx:α Ay:α) = B] = [(λx:α Ap:α) = (λy:α Bp:α)]]
38	3, 10, 15, 25, 37	insti 114	. . 3 ⊢ ⊤⊧[(λx:α Ap:α) = (λy:α Bp:α)]
39	4, 38	leq 91	. 2 ⊢ ⊤⊧[λp:α (λx:α Ap:α) = λp:α (λy:α Bp:α)]
40	2	eta 178	. 2 ⊢ ⊤⊧[λp:α (λx:α Ap:α) = λx:α A]
41	8	eta 178	. 2 ⊢ ⊤⊧[λp:α (λy:α Bp:α) = λy:α B]
42	5, 39, 40, 41	3eqtr3i 97	1 ⊢ ⊤⊧[λx:α A = λy:α B]

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