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	|- T. |= [[x:al = y:al] ==> [(A.\y:al A) ==> (A.\x:al [[x:al = y:al] ==> A])]]

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

Proof of Theorem ax11

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

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9  kct 10   |= wffMMJ2 11  wffMMJ2t 12   ==> tim 121  A.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)