Theorem ax11 201

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.

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 124	. . . . . . . 8 ⊢ ∀:((α → ∗) → ∗)
2		ax11.1	. . . . . . . . 9 ⊢ A:∗
3	2	wl 59	. . . . . . . 8 ⊢ λy:α A:(α → ∗)
4	1, 3	wc 45	. . . . . . 7 ⊢ (∀λy:α A):∗
5	4	id 25	. . . . . 6 ⊢ (∀λy:α A)⊧(∀λy:α A)
6		wv 58	. . . . . . . . . 10 ⊢ x:α:α
7	3, 6	wc 45	. . . . . . . . 9 ⊢ (λy:α Ax:α):∗
8	7	wl 59	. . . . . . . 8 ⊢ λx:α (λy:α Ax:α):(α → ∗)
9	3	eta 166	. . . . . . . 8 ⊢ ⊤⊧[λx:α (λy:α Ax:α) = λy:α A]
10	1, 8, 9	ceq2 80	. . . . . . 7 ⊢ ⊤⊧[(∀λx:α (λy:α Ax:α)) = (∀λy:α A)]
11	4, 10	a1i 28	. . . . . 6 ⊢ (∀λy:α A)⊧[(∀λx:α (λy:α Ax:α)) = (∀λy:α A)]
12	5, 11	mpbir 77	. . . . 5 ⊢ (∀λy:α A)⊧(∀λx:α (λy:α Ax:α))
13		wim 127	. . . . . . . . 9 ⊢ ⇒ :(∗ → (∗ → ∗))
14		wv 58	. . . . . . . . . 10 ⊢ y:α:α
15	6, 14	weqi 68	. . . . . . . . 9 ⊢ [x:α = y:α]:∗
16	13, 15, 2	wov 64	. . . . . . . 8 ⊢ [[x:α = y:α] ⇒ A]:∗
17	16	wl 59	. . . . . . 7 ⊢ λx:α [[x:α = y:α] ⇒ A]:(α → ∗)
18	1, 17	wc 45	. . . . . 6 ⊢ (∀λx:α [[x:α = y:α] ⇒ A]):∗
19	1, 8	wc 45	. . . . . . 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 77	. . . . . . . . . 10 ⊢ ([x:α = y:α], (∀λy:α A))⊧(∀λx:α (λy:α Ax:α))
25	24	ax-cb2 30	. . . . . . . . 9 ⊢ (∀λx:α (λy:α Ax:α)):∗
26	13, 25, 18	wov 64	. . . . . . . 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 80	. . . . . . . . . . . . . 14 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧[(λy:α Ax:α) = (λy:α Ay:α)]
30	7, 15	wct 44	. . . . . . . . . . . . . . 15 ⊢ ((λy:α Ax:α), [x:α = y:α]):∗
31	2	beta 82	. . . . . . . . . . . . . . 15 ⊢ ⊤⊧[(λy:α Ay:α) = A]
32	30, 31	a1i 28	. . . . . . . . . . . . . 14 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧[(λy:α Ay:α) = A]
33	7, 29, 32	eqtri 85	. . . . . . . . . . . . 13 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧[(λy:α Ax:α) = A]
34	27, 33	mpbi 72	. . . . . . . . . . . 12 ⊢ ((λy:α Ax:α), [x:α = y:α])⊧A
35	34	ex 148	. . . . . . . . . . 11 ⊢ (λy:α Ax:α)⊧[[x:α = y:α] ⇒ A]
36		wtru 40	. . . . . . . . . . 11 ⊢ ⊤:∗
37	35, 36	adantl 51	. . . . . . . . . 10 ⊢ (⊤, (λy:α Ax:α))⊧[[x:α = y:α] ⇒ A]
38	37	ex 148	. . . . . . . . 9 ⊢ ⊤⊧[(λy:α Ax:α) ⇒ [[x:α = y:α] ⇒ A]]
39	38	alrimiv 141	. . . . . . . 8 ⊢ ⊤⊧(∀λx:α [(λy:α Ax:α) ⇒ [[x:α = y:α] ⇒ A]])
40	7, 16	ax5 194	. . . . . . . 8 ⊢ ⊤⊧[(∀λx:α [(λy:α Ax:α) ⇒ [[x:α = y:α] ⇒ A]]) ⇒ [(∀λx:α (λy:α Ax:α)) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]]
41	26, 39, 40	mpd 146	. . . . . . 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 146	. . . . 5 ⊢ (∀λx:α (λy:α Ax:α))⊧(∀λx:α [[x:α = y:α] ⇒ A])
44	12, 43	syl 16	. . . 4 ⊢ (∀λy:α A)⊧(∀λx:α [[x:α = y:α] ⇒ A])
45	36, 15	wct 44	. . . 4 ⊢ (⊤, [x:α = y:α]):∗
46	44, 45	adantl 51	. . 3 ⊢ ((⊤, [x:α = y:α]), (∀λy:α A))⊧(∀λx:α [[x:α = y:α] ⇒ A])
47	46	ex 148	. 2 ⊢ (⊤, [x:α = y:α])⊧[(∀λy:α A) ⇒ (∀λx:α [[x:α = y:α] ⇒ A])]
48	47	ex 148	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 111  ∀tal 112

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-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103  ax-eta 165

This theorem depends on definitions:  df-ov 65  df-al 116  df-an 118  df-im 119

This theorem is referenced by: (None)