Theorem ax11 214

Description: Axiom of Variable Substitution. It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. (Contributed by Mario Carneiro, 10-Oct-2014.)

Hypothesis

Ref	Expression
ax11.1	⊢ A:∗

Assertion

Ref	Expression
ax11	⊢ ⊤⊧[[x:α = y:α] ⇒ [(∀λy:α A) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]]

Distinct variable groups:   x,A   x,y,α

Proof of Theorem ax11

Step	Hyp	Ref	Expression
1		wal 134	. . . . . . . 8 ⊢ ∀:((α → ∗) → ∗)
2		ax11.1	. . . . . . . . 9 ⊢ A:∗
3	2	wl 66	. . . . . . . 8 ⊢ λy:α A:(α → ∗)
4	1, 3	wc 50	. . . . . . 7 ⊢ (∀λy:α A):∗
5	4	id 25	. . . . . 6 ⊢ (∀λy:α A)⊧(∀λy:α A)
6		wv 64	. . . . . . . . . 10 ⊢ x:α:α
7	3, 6	wc 50	. . . . . . . . 9 ⊢ (λy:α Ax:α):∗
8	7	wl 66	. . . . . . . 8 ⊢ λx:α (λy:α Ax:α):(α → ∗)
9	3	eta 178	. . . . . . . 8 ⊢ ⊤⊧[λx:α (λy:α Ax:α) = λy:α A]
10	1, 8, 9	ceq2 90	. . . . . . 7 ⊢ ⊤⊧[(∀λx:α (λy:α Ax:α)) = (∀λy:α A)]
11	4, 10	a1i 28	. . . . . 6 ⊢ (∀λy:α A)⊧[(∀λx:α (λy:α Ax:α)) = (∀λy:α A)]
12	5, 11	mpbir 87	. . . . 5 ⊢ (∀λy:α A)⊧(∀λx:α (λy:α Ax:α))
13		wim 137	. . . . . . . . 9 ⊢ ⇒ :(∗ → (∗ → ∗))
14		wv 64	. . . . . . . . . 10 ⊢ y:α:α
15	6, 14	weqi 76	. . . . . . . . 9 ⊢ [x:α = y:α]:∗
16	13, 15, 2	wov 72	. . . . . . . 8 ⊢ [[x:α = y:α] ⇒ A]:∗
17	16	wl 66	. . . . . . 7 ⊢ λx:α [[x:α = y:α] ⇒ A]:(α → ∗)
18	1, 17	wc 50	. . . . . 6 ⊢ (∀λx:α [[x:α = y:α] ⇒ A]):∗
19	1, 8	wc 50	. . . . . . 7 ⊢ (∀λx:α (λy:α Ax:α)):∗
20	19	id 25	. . . . . 6 ⊢ (∀λx:α (λy:α Ax:α))⊧(∀λx:α (λy:α Ax:α))
21	15, 4	simpr 23	. . . . . . . . . . 11 ⊢ ([x:α = y:α], (∀λy:α A))⊧(∀λy:α A)
22	21	ax-cb1 29	. . . . . . . . . . . 12 ⊢ ([x:α = y:α], (∀λy:α A)):∗
23	22, 10	a1i 28	. . . . . . . . . . 11 ⊢ ([x:α = y:α], (∀λy:α A))⊧[(∀λx:α (λy:α Ax:α)) = (∀λy:α A)]
24	21, 23	mpbir 87	. . . . . . . . . 10 ⊢ ([x:α = y:α], (∀λy:α A))⊧(∀λx:α (λy:α Ax:α))
25	24	ax-cb2 30	. . . . . . . . 9 ⊢ (∀λx:α (λy:α Ax:α)):∗
26	13, 25, 18	wov 72	. . . . . . . 8 ⊢ [(∀λx:α (λy:α Ax:α)) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]:∗
27	7, 15	simpl 22	. . . . . . . . . . . . 13 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧(λy:α Ax:α)
28	7, 15	simpr 23	. . . . . . . . . . . . . . 15 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧[x:α = y:α]
29	3, 6, 28	ceq2 90	. . . . . . . . . . . . . 14 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧[(λy:α Ax:α) = (λy:α Ay:α)]
30	7, 15	wct 48	. . . . . . . . . . . . . . 15 ⊢ ((λy:α Ax:α), [x:α = y:α]):∗
31	2	beta 92	. . . . . . . . . . . . . . 15 ⊢ ⊤⊧[(λy:α Ay:α) = A]
32	30, 31	a1i 28	. . . . . . . . . . . . . 14 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧[(λy:α Ay:α) = A]
33	7, 29, 32	eqtri 95	. . . . . . . . . . . . 13 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧[(λy:α Ax:α) = A]
34	27, 33	mpbi 82	. . . . . . . . . . . 12 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧A
35	34	ex 158	. . . . . . . . . . 11 ⊢ (λy:α Ax:α)⊧[[x:α = y:α] ⇒ A]
36		wtru 43	. . . . . . . . . . 11 ⊢ ⊤:∗
37	35, 36	adantl 56	. . . . . . . . . 10 ⊢ (⊤, (λy:α Ax:α))⊧[[x:α = y:α] ⇒ A]
38	37	ex 158	. . . . . . . . 9 ⊢ ⊤⊧[(λy:α Ax:α) ⇒ [[x:α = y:α] ⇒ A]]
39	38	alrimiv 151	. . . . . . . 8 ⊢ ⊤⊧(∀λx:α [(λy:α Ax:α) ⇒ [[x:α = y:α] ⇒ A]])
40	7, 16	ax5 207	. . . . . . . 8 ⊢ ⊤⊧[(∀λx:α [(λy:α Ax:α) ⇒ [[x:α = y:α] ⇒ A]]) ⇒ [(∀λx:α (λy:α Ax:α)) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]]
41	26, 39, 40	mpd 156	. . . . . . 7 ⊢ ⊤⊧[(∀λx:α (λy:α Ax:α)) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]
42	19, 41	a1i 28	. . . . . 6 ⊢ (∀λx:α (λy:α Ax:α))⊧[(∀λx:α (λy:α Ax:α)) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]
43	18, 20, 42	mpd 156	. . . . 5 ⊢ (∀λx:α (λy:α Ax:α))⊧(∀λx:α [[x:α = y:α] ⇒ A])
44	12, 43	syl 16	. . . 4 ⊢ (∀λy:α A)⊧(∀λx:α [[x:α = y:α] ⇒ A])
45	36, 15	wct 48	. . . 4 ⊢ (⊤, [x:α = y:α]):∗
46	44, 45	adantl 56	. . 3 ⊢ ((⊤, [x:α = y:α]), (∀λy:α A))⊧(∀λx:α [[x:α = y:α] ⇒ A])
47	46	ex 158	. 2 ⊢ (⊤, [x:α = y:α])⊧[(∀λy:α A) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]
48	47	ex 158	1 ⊢ ⊤⊧[[x:α = y:α] ⇒ [(∀λy:α A) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]]

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  kct 10  ⊧wffMMJ2 11  wffMMJ2t 12   ⇒ tim 121  ∀tal 122

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  df-an 128  df-im 129

This theorem is referenced by: (None)