Theorem exlimd 171

Description: Existential elimination.

Hypotheses

Ref	Expression
exlimd.1	|- (R, A) |= T
exlimd.2	|- T. |= [(\x:al Ry:al) = R]
exlimd.3	|- T. |= [(\x:al Ty:al) = T]

Assertion

Ref	Expression
exlimd	|- (R, (E.\x:al A)) |= T

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

Proof of Theorem exlimd

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exlimd.1	. . 3 |- (R, A) |= T
2	1	ax-cb2 30	. 2 |- T:*
3		wim 127	. . . . . 6 |- ==> :(* -> (* -> *))
4	1	ax-cb1 29	. . . . . . . . 9 |- (R, A):*
5	4	wctr 32	. . . . . . . 8 |- A:*
6	5	wl 59	. . . . . . 7 |- \x:al A:(al -> *)
7		wv 58	. . . . . . 7 |- z:al:al
8	6, 7	wc 45	. . . . . 6 |- (\x:al Az:al):*
9	3, 8, 2	wov 64	. . . . 5 |- [(\x:al Az:al) ==> T]:*
10	4	wctl 31	. . . . . 6 |- R:*
11	10	id 25	. . . . 5 |- R |= R
12	3, 10, 9	wov 64	. . . . . . 7 |- [R ==> [(\x:al Az:al) ==> T]]:*
13	1	ex 148	. . . . . . . . 9 |- R |= [A ==> T]
14		wtru 40	. . . . . . . . 9 |- T.:*
15	13, 14	adantl 51	. . . . . . . 8 |- (T., R) |= [A ==> T]
16	15	ex 148	. . . . . . 7 |- T. |= [R ==> [A ==> T]]
17		wv 58	. . . . . . . 8 |- y:al:al
18	3, 17	ax-17 95	. . . . . . . 8 |- T. |= [(\x:al ==> y:al) = ==> ]
19		exlimd.2	. . . . . . . 8 |- T. |= [(\x:al Ry:al) = R]
20	5, 17	ax-hbl1 93	. . . . . . . . . 10 |- T. |= [(\x:al \x:al Ay:al) = \x:al A]
21	7, 17	ax-17 95	. . . . . . . . . 10 |- T. |= [(\x:al z:aly:al) = z:al]
22	6, 7, 17, 20, 21	hbc 100	. . . . . . . . 9 |- T. |= [(\x:al (\x:al Az:al)y:al) = (\x:al Az:al)]
23		exlimd.3	. . . . . . . . 9 |- T. |= [(\x:al Ty:al) = T]
24	3, 8, 17, 2, 18, 22, 23	hbov 101	. . . . . . . 8 |- T. |= [(\x:al [(\x:al Az:al) ==> T]y:al) = [(\x:al Az:al) ==> T]]
25	3, 10, 17, 9, 18, 19, 24	hbov 101	. . . . . . 7 |- T. |= [(\x:al [R ==> [(\x:al Az:al) ==> T]]y:al) = [R ==> [(\x:al Az:al) ==> T]]]
26	3, 5, 2	wov 64	. . . . . . . 8 |- [A ==> T]:*
27		wv 58	. . . . . . . . . . . 12 |- x:al:al
28	27, 7	weqi 68	. . . . . . . . . . 11 |- [x:al = z:al]:*
29	6, 27	wc 45	. . . . . . . . . . . 12 |- (\x:al Ax:al):*
30	5	beta 82	. . . . . . . . . . . 12 |- T. |= [(\x:al Ax:al) = A]
31	29, 30	eqcomi 70	. . . . . . . . . . 11 |- T. |= [A = (\x:al Ax:al)]
32	28, 31	a1i 28	. . . . . . . . . 10 |- [x:al = z:al] |= [A = (\x:al Ax:al)]
33	28	id 25	. . . . . . . . . . 11 |- [x:al = z:al] |= [x:al = z:al]
34	6, 27, 33	ceq2 80	. . . . . . . . . 10 |- [x:al = z:al] |= [(\x:al Ax:al) = (\x:al Az:al)]
35	5, 32, 34	eqtri 85	. . . . . . . . 9 |- [x:al = z:al] |= [A = (\x:al Az:al)]
36	3, 5, 2, 35	oveq1 89	. . . . . . . 8 |- [x:al = z:al] |= [[A ==> T] = [(\x:al Az:al) ==> T]]
37	3, 10, 26, 36	oveq2 91	. . . . . . 7 |- [x:al = z:al] |= [[R ==> [A ==> T]] = [R ==> [(\x:al Az:al) ==> T]]]
38	7, 12, 16, 25, 37	insti 104	. . . . . 6 |- T. |= [R ==> [(\x:al Az:al) ==> T]]
39	10, 38	a1i 28	. . . . 5 |- R |= [R ==> [(\x:al Az:al) ==> T]]
40	9, 11, 39	mpd 146	. . . 4 |- R |= [(\x:al Az:al) ==> T]
41	40	alrimiv 141	. . 3 |- R |= (A.\z:al [(\x:al Az:al) ==> T])
42		wex 129	. . . 4 |- E.:((al -> *) -> *)
43	42, 6	wc 45	. . 3 |- (E.\x:al A):*
44	41, 43	adantr 50	. 2 |- (R, (E.\x:al A)) |= (A.\z:al [(\x:al Az:al) ==> T])
45	10, 43	simpr 23	. . . 4 |- (R, (E.\x:al A)) |= (E.\x:al A)
46	44	ax-cb1 29	. . . . 5 |- (R, (E.\x:al A)):*
47	6	exval 133	. . . . 5 |- T. |= [(E.\x:al A) = (A.\y:* [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*])]
48	46, 47	a1i 28	. . . 4 |- (R, (E.\x:al A)) |= [(E.\x:al A) = (A.\y:* [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*])]
49	45, 48	mpbi 72	. . 3 |- (R, (E.\x:al A)) |= (A.\y:* [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*])
50		wal 124	. . . . . 6 |- A.:((al -> *) -> *)
51		wv 58	. . . . . . . 8 |- y:*:*
52	3, 8, 51	wov 64	. . . . . . 7 |- [(\x:al Az:al) ==> y:*]:*
53	52	wl 59	. . . . . 6 |- \z:al [(\x:al Az:al) ==> y:*]:(al -> *)
54	50, 53	wc 45	. . . . 5 |- (A.\z:al [(\x:al Az:al) ==> y:*]):*
55	3, 54, 51	wov 64	. . . 4 |- [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*]:*
56	51, 2	weqi 68	. . . . . . . . 9 |- [y:* = T]:*
57	56	id 25	. . . . . . . 8 |- [y:* = T] |= [y:* = T]
58	3, 8, 51, 57	oveq2 91	. . . . . . 7 |- [y:* = T] |= [[(\x:al Az:al) ==> y:*] = [(\x:al Az:al) ==> T]]
59	52, 58	leq 81	. . . . . 6 |- [y:* = T] |= [\z:al [(\x:al Az:al) ==> y:*] = \z:al [(\x:al Az:al) ==> T]]
60	50, 53, 59	ceq2 80	. . . . 5 |- [y:* = T] |= [(A.\z:al [(\x:al Az:al) ==> y:*]) = (A.\z:al [(\x:al Az:al) ==> T])]
61	3, 54, 51, 60, 57	oveq12 90	. . . 4 |- [y:* = T] |= [[(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*] = [(A.\z:al [(\x:al Az:al) ==> T]) ==> T]]
62	55, 2, 61	cla4v 142	. . 3 |- (A.\y:* [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*]) |= [(A.\z:al [(\x:al Az:al) ==> T]) ==> T]
63	49, 62	syl 16	. 2 |- (R, (E.\x:al A)) |= [(A.\z:al [(\x:al Az:al) ==> T]) ==> T]
64	2, 44, 63	mpd 146	1 |- (R, (E.\x:al A)) |= T

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9  kct 10   |= wffMMJ2 11   ==> tim 111  A.tal 112  E.tex 113

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

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

This theorem is referenced by:  eximdv  173  alnex  174