Theorem exlimdv2 156

Description: Existential elimination.

Hypotheses

Ref	Expression
exlimdv2.1	|- F:(al -> *)
exlimdv2.2	|- (R, (Fx:al)) |= T

Assertion

Ref	Expression
exlimdv2	|- (R, (E.F)) |= T

Distinct variable groups:   x,F   x,R   x,T   al,x

Proof of Theorem exlimdv2

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exlimdv2.2	. . 3 |- (R, (Fx:al)) |= T
2	1	ax-cb2 30	. 2 |- T:*
3	1	ex 148	. . . 4 |- R |= [(Fx:al) ==> T]
4	3	alrimiv 141	. . 3 |- R |= (A.\x:al [(Fx:al) ==> T])
5		wex 129	. . . 4 |- E.:((al -> *) -> *)
6		exlimdv2.1	. . . 4 |- F:(al -> *)
7	5, 6	wc 45	. . 3 |- (E.F):*
8	4, 7	adantr 50	. 2 |- (R, (E.F)) |= (A.\x:al [(Fx:al) ==> T])
9	1	ax-cb1 29	. . . . . 6 |- (R, (Fx:al)):*
10	9	wctl 31	. . . . 5 |- R:*
11	10, 7	simpr 23	. . . 4 |- (R, (E.F)) |= (E.F)
12	10, 7	wct 44	. . . . 5 |- (R, (E.F)):*
13	6	exval 133	. . . . 5 |- T. |= [(E.F) = (A.\p:* [(A.\x:al [(Fx:al) ==> p:*]) ==> p:*])]
14	12, 13	a1i 28	. . . 4 |- (R, (E.F)) |= [(E.F) = (A.\p:* [(A.\x:al [(Fx:al) ==> p:*]) ==> p:*])]
15	11, 14	mpbi 72	. . 3 |- (R, (E.F)) |= (A.\p:* [(A.\x:al [(Fx:al) ==> p:*]) ==> p:*])
16		wim 127	. . . . 5 |- ==> :(* -> (* -> *))
17		wal 124	. . . . . 6 |- A.:((al -> *) -> *)
18		wv 58	. . . . . . . . 9 |- x:al:al
19	6, 18	wc 45	. . . . . . . 8 |- (Fx:al):*
20		wv 58	. . . . . . . 8 |- p:*:*
21	16, 19, 20	wov 64	. . . . . . 7 |- [(Fx:al) ==> p:*]:*
22	21	wl 59	. . . . . 6 |- \x:al [(Fx:al) ==> p:*]:(al -> *)
23	17, 22	wc 45	. . . . 5 |- (A.\x:al [(Fx:al) ==> p:*]):*
24	16, 23, 20	wov 64	. . . 4 |- [(A.\x:al [(Fx:al) ==> p:*]) ==> p:*]:*
25	20, 2	weqi 68	. . . . . . . . 9 |- [p:* = T]:*
26	25	id 25	. . . . . . . 8 |- [p:* = T] |= [p:* = T]
27	16, 19, 20, 26	oveq2 91	. . . . . . 7 |- [p:* = T] |= [[(Fx:al) ==> p:*] = [(Fx:al) ==> T]]
28	21, 27	leq 81	. . . . . 6 |- [p:* = T] |= [\x:al [(Fx:al) ==> p:*] = \x:al [(Fx:al) ==> T]]
29	17, 22, 28	ceq2 80	. . . . 5 |- [p:* = T] |= [(A.\x:al [(Fx:al) ==> p:*]) = (A.\x:al [(Fx:al) ==> T])]
30	16, 23, 20, 29, 26	oveq12 90	. . . 4 |- [p:* = T] |= [[(A.\x:al [(Fx:al) ==> p:*]) ==> p:*] = [(A.\x:al [(Fx:al) ==> T]) ==> T]]
31	24, 2, 30	cla4v 142	. . 3 |- (A.\p:* [(A.\x:al [(Fx:al) ==> p:*]) ==> p:*]) |= [(A.\x:al [(Fx:al) ==> T]) ==> T]
32	15, 31	syl 16	. 2 |- (R, (E.F)) |= [(A.\x:al [(Fx:al) ==> T]) ==> T]
33	2, 8, 32	mpd 146	1 |- (R, (E.F)) |= T

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  [kbr 9  kct 10   |= wffMMJ2 11  wffMMJ2t 12   ==> 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:  exlimdv  157  dfex2  185