Theorem exlimdv2 166

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

Hypotheses

Ref	Expression
exlimdv2.1	⊢ F:(α → ∗)
exlimdv2.2	⊢ (R, (Fx:α))⊧T

Assertion

Ref	Expression
exlimdv2	⊢ (R, (∃F))⊧T

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

Proof of Theorem exlimdv2

Dummy variable p is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exlimdv2.2	. . 3 ⊢ (R, (Fx:α))⊧T
2	1	ax-cb2 30	. 2 ⊢ T:∗
3	1	ex 158	. . . 4 ⊢ R⊧[(Fx:α) ⇒ T]
4	3	alrimiv 151	. . 3 ⊢ R⊧(∀λx:α [(Fx:α) ⇒ T])
5		wex 139	. . . 4 ⊢ ∃:((α → ∗) → ∗)
6		exlimdv2.1	. . . 4 ⊢ F:(α → ∗)
7	5, 6	wc 50	. . 3 ⊢ (∃F):∗
8	4, 7	adantr 55	. 2 ⊢ (R, (∃F))⊧(∀λx:α [(Fx:α) ⇒ T])
9	1	ax-cb1 29	. . . . . 6 ⊢ (R, (Fx:α)):∗
10	9	wctl 33	. . . . 5 ⊢ R:∗
11	10, 7	simpr 23	. . . 4 ⊢ (R, (∃F))⊧(∃F)
12	10, 7	wct 48	. . . . 5 ⊢ (R, (∃F)):∗
13	6	exval 143	. . . . 5 ⊢ ⊤⊧[(∃F) = (∀λp:∗ [(∀λx:α [(Fx:α) ⇒ p:∗]) ⇒ p:∗])]
14	12, 13	a1i 28	. . . 4 ⊢ (R, (∃F))⊧[(∃F) = (∀λp:∗ [(∀λx:α [(Fx:α) ⇒ p:∗]) ⇒ p:∗])]
15	11, 14	mpbi 82	. . 3 ⊢ (R, (∃F))⊧(∀λp:∗ [(∀λx:α [(Fx:α) ⇒ p:∗]) ⇒ p:∗])
16		wim 137	. . . . 5 ⊢ ⇒ :(∗ → (∗ → ∗))
17		wal 134	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
18		wv 64	. . . . . . . . 9 ⊢ x:α:α
19	6, 18	wc 50	. . . . . . . 8 ⊢ (Fx:α):∗
20		wv 64	. . . . . . . 8 ⊢ p:∗:∗
21	16, 19, 20	wov 72	. . . . . . 7 ⊢ [(Fx:α) ⇒ p:∗]:∗
22	21	wl 66	. . . . . 6 ⊢ λx:α [(Fx:α) ⇒ p:∗]:(α → ∗)
23	17, 22	wc 50	. . . . 5 ⊢ (∀λx:α [(Fx:α) ⇒ p:∗]):∗
24	16, 23, 20	wov 72	. . . 4 ⊢ [(∀λx:α [(Fx:α) ⇒ 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:α) ⇒ p:∗] = [(Fx:α) ⇒ T]]
28	21, 27	leq 91	. . . . . 6 ⊢ [p:∗ = T]⊧[λx:α [(Fx:α) ⇒ p:∗] = λx:α [(Fx:α) ⇒ T]]
29	17, 22, 28	ceq2 90	. . . . 5 ⊢ [p:∗ = T]⊧[(∀λx:α [(Fx:α) ⇒ p:∗]) = (∀λx:α [(Fx:α) ⇒ T])]
30	16, 23, 20, 29, 26	oveq12 100	. . . 4 ⊢ [p:∗ = T]⊧[[(∀λx:α [(Fx:α) ⇒ p:∗]) ⇒ p:∗] = [(∀λx:α [(Fx:α) ⇒ T]) ⇒ T]]
31	24, 2, 30	cla4v 152	. . 3 ⊢ (∀λp:∗ [(∀λx:α [(Fx:α) ⇒ p:∗]) ⇒ p:∗])⊧[(∀λx:α [(Fx:α) ⇒ T]) ⇒ T]
32	15, 31	syl 16	. 2 ⊢ (R, (∃F))⊧[(∀λx:α [(Fx:α) ⇒ T]) ⇒ T]
33	2, 8, 32	mpd 156	1 ⊢ (R, (∃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  ∀tal 122  ∃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