Theorem exlimdv2 156

Description: Existential elimination.

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 148	. . . 4 ⊢ R⊧[(Fx:α) ⇒ T]
4	3	alrimiv 141	. . 3 ⊢ R⊧(∀λx:α [(Fx:α) ⇒ T])
5		wex 129	. . . 4 ⊢ ∃:((α → ∗) → ∗)
6		exlimdv2.1	. . . 4 ⊢ F:(α → ∗)
7	5, 6	wc 45	. . 3 ⊢ (∃F):∗
8	4, 7	adantr 50	. 2 ⊢ (R, (∃F))⊧(∀λx:α [(Fx:α) ⇒ T])
9	1	ax-cb1 29	. . . . . 6 ⊢ (R, (Fx:α)):∗
10	9	wctl 31	. . . . 5 ⊢ R:∗
11	10, 7	simpr 23	. . . 4 ⊢ (R, (∃F))⊧(∃F)
12	10, 7	wct 44	. . . . 5 ⊢ (R, (∃F)):∗
13	6	exval 133	. . . . 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 72	. . 3 ⊢ (R, (∃F))⊧(∀λp:∗ [(∀λx:α [(Fx:α) ⇒ p:∗]) ⇒ p:∗])
16		wim 127	. . . . 5 ⊢ ⇒ :(∗ → (∗ → ∗))
17		wal 124	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
18		wv 58	. . . . . . . . 9 ⊢ x:α:α
19	6, 18	wc 45	. . . . . . . 8 ⊢ (Fx:α):∗
20		wv 58	. . . . . . . 8 ⊢ p:∗:∗
21	16, 19, 20	wov 64	. . . . . . 7 ⊢ [(Fx:α) ⇒ p:∗]:∗
22	21	wl 59	. . . . . 6 ⊢ λx:α [(Fx:α) ⇒ p:∗]:(α → ∗)
23	17, 22	wc 45	. . . . 5 ⊢ (∀λx:α [(Fx:α) ⇒ p:∗]):∗
24	16, 23, 20	wov 64	. . . 4 ⊢ [(∀λx:α [(Fx:α) ⇒ 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:α) ⇒ p:∗] = [(Fx:α) ⇒ T]]
28	21, 27	leq 81	. . . . . 6 ⊢ [p:∗ = T]⊧[λx:α [(Fx:α) ⇒ p:∗] = λx:α [(Fx:α) ⇒ T]]
29	17, 22, 28	ceq2 80	. . . . 5 ⊢ [p:∗ = T]⊧[(∀λx:α [(Fx:α) ⇒ p:∗]) = (∀λx:α [(Fx:α) ⇒ T])]
30	16, 23, 20, 29, 26	oveq12 90	. . . 4 ⊢ [p:∗ = T]⊧[[(∀λx:α [(Fx:α) ⇒ p:∗]) ⇒ p:∗] = [(∀λx:α [(Fx:α) ⇒ T]) ⇒ T]]
31	24, 2, 30	cla4v 142	. . 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 146	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 111  ∀tal 112  ∃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