Theorem exlimd 183

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

Hypotheses

Ref	Expression
exlimd.1	⊢ (R, A)⊧T
exlimd.2	⊢ ⊤⊧[(λx:α Ry:α) = R]
exlimd.3	⊢ ⊤⊧[(λx:α Ty:α) = T]

Assertion

Ref	Expression
exlimd	⊢ (R, (∃λx:α A))⊧T

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

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 137	. . . . . 6 ⊢ ⇒ :(∗ → (∗ → ∗))
4	1	ax-cb1 29	. . . . . . . . 9 ⊢ (R, A):∗
5	4	wctr 34	. . . . . . . 8 ⊢ A:∗
6	5	wl 66	. . . . . . 7 ⊢ λx:α A:(α → ∗)
7		wv 64	. . . . . . 7 ⊢ z:α:α
8	6, 7	wc 50	. . . . . 6 ⊢ (λx:α Az:α):∗
9	3, 8, 2	wov 72	. . . . 5 ⊢ [(λx:α Az:α) ⇒ T]:∗
10	4	wctl 33	. . . . . 6 ⊢ R:∗
11	10	id 25	. . . . 5 ⊢ R⊧R
12	3, 10, 9	wov 72	. . . . . . 7 ⊢ [R ⇒ [(λx:α Az:α) ⇒ T]]:∗
13	1	ex 158	. . . . . . . . 9 ⊢ R⊧[A ⇒ T]
14		wtru 43	. . . . . . . . 9 ⊢ ⊤:∗
15	13, 14	adantl 56	. . . . . . . 8 ⊢ (⊤, R)⊧[A ⇒ T]
16	15	ex 158	. . . . . . 7 ⊢ ⊤⊧[R ⇒ [A ⇒ T]]
17		wv 64	. . . . . . . 8 ⊢ y:α:α
18	3, 17	ax-17 105	. . . . . . . 8 ⊢ ⊤⊧[(λx:α ⇒ y:α) = ⇒ ]
19		exlimd.2	. . . . . . . 8 ⊢ ⊤⊧[(λx:α Ry:α) = R]
20	5, 17	ax-hbl1 103	. . . . . . . . . 10 ⊢ ⊤⊧[(λx:α λx:α Ay:α) = λx:α A]
21	7, 17	ax-17 105	. . . . . . . . . 10 ⊢ ⊤⊧[(λx:α z:αy:α) = z:α]
22	6, 7, 17, 20, 21	hbc 110	. . . . . . . . 9 ⊢ ⊤⊧[(λx:α (λx:α Az:α)y:α) = (λx:α Az:α)]
23		exlimd.3	. . . . . . . . 9 ⊢ ⊤⊧[(λx:α Ty:α) = T]
24	3, 8, 17, 2, 18, 22, 23	hbov 111	. . . . . . . 8 ⊢ ⊤⊧[(λx:α [(λx:α Az:α) ⇒ T]y:α) = [(λx:α Az:α) ⇒ T]]
25	3, 10, 17, 9, 18, 19, 24	hbov 111	. . . . . . 7 ⊢ ⊤⊧[(λx:α [R ⇒ [(λx:α Az:α) ⇒ T]]y:α) = [R ⇒ [(λx:α Az:α) ⇒ T]]]
26	3, 5, 2	wov 72	. . . . . . . 8 ⊢ [A ⇒ T]:∗
27		wv 64	. . . . . . . . . . . 12 ⊢ x:α:α
28	27, 7	weqi 76	. . . . . . . . . . 11 ⊢ [x:α = z:α]:∗
29	6, 27	wc 50	. . . . . . . . . . . 12 ⊢ (λx:α Ax:α):∗
30	5	beta 92	. . . . . . . . . . . 12 ⊢ ⊤⊧[(λx:α Ax:α) = A]
31	29, 30	eqcomi 79	. . . . . . . . . . 11 ⊢ ⊤⊧[A = (λx:α Ax:α)]
32	28, 31	a1i 28	. . . . . . . . . 10 ⊢ [x:α = z:α]⊧[A = (λx:α Ax:α)]
33	28	id 25	. . . . . . . . . . 11 ⊢ [x:α = z:α]⊧[x:α = z:α]
34	6, 27, 33	ceq2 90	. . . . . . . . . 10 ⊢ [x:α = z:α]⊧[(λx:α Ax:α) = (λx:α Az:α)]
35	5, 32, 34	eqtri 95	. . . . . . . . 9 ⊢ [x:α = z:α]⊧[A = (λx:α Az:α)]
36	3, 5, 2, 35	oveq1 99	. . . . . . . 8 ⊢ [x:α = z:α]⊧[[A ⇒ T] = [(λx:α Az:α) ⇒ T]]
37	3, 10, 26, 36	oveq2 101	. . . . . . 7 ⊢ [x:α = z:α]⊧[[R ⇒ [A ⇒ T]] = [R ⇒ [(λx:α Az:α) ⇒ T]]]
38	7, 12, 16, 25, 37	insti 114	. . . . . 6 ⊢ ⊤⊧[R ⇒ [(λx:α Az:α) ⇒ T]]
39	10, 38	a1i 28	. . . . 5 ⊢ R⊧[R ⇒ [(λx:α Az:α) ⇒ T]]
40	9, 11, 39	mpd 156	. . . 4 ⊢ R⊧[(λx:α Az:α) ⇒ T]
41	40	alrimiv 151	. . 3 ⊢ R⊧(∀λz:α [(λx:α Az:α) ⇒ T])
42		wex 139	. . . 4 ⊢ ∃:((α → ∗) → ∗)
43	42, 6	wc 50	. . 3 ⊢ (∃λx:α A):∗
44	41, 43	adantr 55	. 2 ⊢ (R, (∃λx:α A))⊧(∀λz:α [(λx:α Az:α) ⇒ T])
45	10, 43	simpr 23	. . . 4 ⊢ (R, (∃λx:α A))⊧(∃λx:α A)
46	44	ax-cb1 29	. . . . 5 ⊢ (R, (∃λx:α A)):∗
47	6	exval 143	. . . . 5 ⊢ ⊤⊧[(∃λx:α A) = (∀λy:∗ [(∀λz:α [(λx:α Az:α) ⇒ y:∗]) ⇒ y:∗])]
48	46, 47	a1i 28	. . . 4 ⊢ (R, (∃λx:α A))⊧[(∃λx:α A) = (∀λy:∗ [(∀λz:α [(λx:α Az:α) ⇒ y:∗]) ⇒ y:∗])]
49	45, 48	mpbi 82	. . 3 ⊢ (R, (∃λx:α A))⊧(∀λy:∗ [(∀λz:α [(λx:α Az:α) ⇒ y:∗]) ⇒ y:∗])
50		wal 134	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
51		wv 64	. . . . . . . 8 ⊢ y:∗:∗
52	3, 8, 51	wov 72	. . . . . . 7 ⊢ [(λx:α Az:α) ⇒ y:∗]:∗
53	52	wl 66	. . . . . 6 ⊢ λz:α [(λx:α Az:α) ⇒ y:∗]:(α → ∗)
54	50, 53	wc 50	. . . . 5 ⊢ (∀λz:α [(λx:α Az:α) ⇒ y:∗]):∗
55	3, 54, 51	wov 72	. . . 4 ⊢ [(∀λz:α [(λx:α Az:α) ⇒ y:∗]) ⇒ y:∗]:∗
56	51, 2	weqi 76	. . . . . . . . 9 ⊢ [y:∗ = T]:∗
57	56	id 25	. . . . . . . 8 ⊢ [y:∗ = T]⊧[y:∗ = T]
58	3, 8, 51, 57	oveq2 101	. . . . . . 7 ⊢ [y:∗ = T]⊧[[(λx:α Az:α) ⇒ y:∗] = [(λx:α Az:α) ⇒ T]]
59	52, 58	leq 91	. . . . . 6 ⊢ [y:∗ = T]⊧[λz:α [(λx:α Az:α) ⇒ y:∗] = λz:α [(λx:α Az:α) ⇒ T]]
60	50, 53, 59	ceq2 90	. . . . 5 ⊢ [y:∗ = T]⊧[(∀λz:α [(λx:α Az:α) ⇒ y:∗]) = (∀λz:α [(λx:α Az:α) ⇒ T])]
61	3, 54, 51, 60, 57	oveq12 100	. . . 4 ⊢ [y:∗ = T]⊧[[(∀λz:α [(λx:α Az:α) ⇒ y:∗]) ⇒ y:∗] = [(∀λz:α [(λx:α Az:α) ⇒ T]) ⇒ T]]
62	55, 2, 61	cla4v 152	. . 3 ⊢ (∀λy:∗ [(∀λz:α [(λx:α Az:α) ⇒ y:∗]) ⇒ y:∗])⊧[(∀λz:α [(λx:α Az:α) ⇒ T]) ⇒ T]
63	49, 62	syl 16	. 2 ⊢ (R, (∃λx:α A))⊧[(∀λz:α [(λx:α Az:α) ⇒ T]) ⇒ T]
64	2, 44, 63	mpd 156	1 ⊢ (R, (∃λx:α A))⊧T

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  kct 10  ⊧wffMMJ2 11   ⇒ 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:  eximdv  185  alnex  186