Theorem exlimdv2 166

Description: Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)

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 158	. . . 4 |- R |= [(Fx:al) ==> T]
4	3	alrimiv 151	. . 3 |- R |= (A.\x:al [(Fx:al) ==> T])
5		wex 139	. . . 4 |- E.:((al -> *) -> *)
6		exlimdv2.1	. . . 4 |- F:(al -> *)
7	5, 6	wc 50	. . 3 |- (E.F):*
8	4, 7	adantr 55	. 2 |- (R, (E.F)) |= (A.\x:al [(Fx:al) ==> T])
9	1	ax-cb1 29	. . . . . 6 |- (R, (Fx:al)):*
10	9	wctl 33	. . . . 5 |- R:*
11	10, 7	simpr 23	. . . 4 |- (R, (E.F)) |= (E.F)
12	10, 7	wct 48	. . . . 5 |- (R, (E.F)):*
13	6	exval 143	. . . . 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 82	. . 3 |- (R, (E.F)) |= (A.\p:* [(A.\x:al [(Fx:al) ==> p:*]) ==> p:*])
16		wim 137	. . . . 5 |- ==> :(* -> (* -> *))
17		wal 134	. . . . . 6 |- A.:((al -> *) -> *)
18		wv 64	. . . . . . . . 9 |- x:al:al
19	6, 18	wc 50	. . . . . . . 8 |- (Fx:al):*
20		wv 64	. . . . . . . 8 |- p:*:*
21	16, 19, 20	wov 72	. . . . . . 7 |- [(Fx:al) ==> p:*]:*
22	21	wl 66	. . . . . 6 |- \x:al [(Fx:al) ==> p:*]:(al -> *)
23	17, 22	wc 50	. . . . 5 |- (A.\x:al [(Fx:al) ==> p:*]):*
24	16, 23, 20	wov 72	. . . 4 |- [(A.\x:al [(Fx:al) ==> p:*]) ==> p:*]:*
25	20, 2	weqi 76	. . . . . . . . 9 |- [p:* = T]:*
26	25	id 25	. . . . . . . 8 |- [p:* = T] |= [p:* = T]
27	16, 19, 20, 26	oveq2 101	. . . . . . 7 |- [p:* = T] |= [[(Fx:al) ==> p:*] = [(Fx:al) ==> T]]
28	21, 27	leq 91	. . . . . 6 |- [p:* = T] |= [\x:al [(Fx:al) ==> p:*] = \x:al [(Fx:al) ==> T]]
29	17, 22, 28	ceq2 90	. . . . 5 |- [p:* = T] |= [(A.\x:al [(Fx:al) ==> p:*]) = (A.\x:al [(Fx:al) ==> T])]
30	16, 23, 20, 29, 26	oveq12 100	. . . 4 |- [p:* = T] |= [[(A.\x:al [(Fx:al) ==> p:*]) ==> p:*] = [(A.\x:al [(Fx:al) ==> T]) ==> T]]
31	24, 2, 30	cla4v 152	. . 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 156	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 121  A.tal 122  E.tex 123

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

This theorem depends on definitions:  df-ov 73  df-al 126  df-an 128  df-im 129  df-ex 131

This theorem is referenced by:  exlimdv  167  dfex2  198