HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  exlimd Unicode version

Theorem exlimd 183
Description: Existential elimination. (Contributed by Mario Carneiro, 9-Oct-2014.)
Hypotheses
Ref Expression
exlimd.1 |- (R, A) |= T
exlimd.2 |- T. |= [(\x:al Ry:al) = R]
exlimd.3 |- T. |= [(\x:al Ty:al) = T]
Assertion
Ref Expression
exlimd |- (R, (E.\x:al A)) |= T
Distinct variable groups:   y,A   y,R   y,T   x,y,al

Proof of Theorem exlimd
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 exlimd.1 . . 3 |- (R, A) |= T
21ax-cb2 30 . 2 |- T:*
3 wim 137 . . . . . 6 |- ==> :(* -> (* -> *))
41ax-cb1 29 . . . . . . . . 9 |- (R, A):*
54wctr 34 . . . . . . . 8 |- A:*
65wl 66 . . . . . . 7 |- \x:al A:(al -> *)
7 wv 64 . . . . . . 7 |- z:al:al
86, 7wc 50 . . . . . 6 |- (\x:al Az:al):*
93, 8, 2wov 72 . . . . 5 |- [(\x:al Az:al) ==> T]:*
104wctl 33 . . . . . 6 |- R:*
1110id 25 . . . . 5 |- R |= R
123, 10, 9wov 72 . . . . . . 7 |- [R ==> [(\x:al Az:al) ==> T]]:*
131ex 158 . . . . . . . . 9 |- R |= [A ==> T]
14 wtru 43 . . . . . . . . 9 |- T.:*
1513, 14adantl 56 . . . . . . . 8 |- (T., R) |= [A ==> T]
1615ex 158 . . . . . . 7 |- T. |= [R ==> [A ==> T]]
17 wv 64 . . . . . . . 8 |- y:al:al
183, 17ax-17 105 . . . . . . . 8 |- T. |= [(\x:al ==> y:al) = ==> ]
19 exlimd.2 . . . . . . . 8 |- T. |= [(\x:al Ry:al) = R]
205, 17ax-hbl1 103 . . . . . . . . . 10 |- T. |= [(\x:al \x:al Ay:al) = \x:al A]
217, 17ax-17 105 . . . . . . . . . 10 |- T. |= [(\x:al z:aly:al) = z:al]
226, 7, 17, 20, 21hbc 110 . . . . . . . . 9 |- T. |= [(\x:al (\x:al Az:al)y:al) = (\x:al Az:al)]
23 exlimd.3 . . . . . . . . 9 |- T. |= [(\x:al Ty:al) = T]
243, 8, 17, 2, 18, 22, 23hbov 111 . . . . . . . 8 |- T. |= [(\x:al [(\x:al Az:al) ==> T]y:al) = [(\x:al Az:al) ==> T]]
253, 10, 17, 9, 18, 19, 24hbov 111 . . . . . . 7 |- T. |= [(\x:al [R ==> [(\x:al Az:al) ==> T]]y:al) = [R ==> [(\x:al Az:al) ==> T]]]
263, 5, 2wov 72 . . . . . . . 8 |- [A ==> T]:*
27 wv 64 . . . . . . . . . . . 12 |- x:al:al
2827, 7weqi 76 . . . . . . . . . . 11 |- [x:al = z:al]:*
296, 27wc 50 . . . . . . . . . . . 12 |- (\x:al Ax:al):*
305beta 92 . . . . . . . . . . . 12 |- T. |= [(\x:al Ax:al) = A]
3129, 30eqcomi 79 . . . . . . . . . . 11 |- T. |= [A = (\x:al Ax:al)]
3228, 31a1i 28 . . . . . . . . . 10 |- [x:al = z:al] |= [A = (\x:al Ax:al)]
3328id 25 . . . . . . . . . . 11 |- [x:al = z:al] |= [x:al = z:al]
346, 27, 33ceq2 90 . . . . . . . . . 10 |- [x:al = z:al] |= [(\x:al Ax:al) = (\x:al Az:al)]
355, 32, 34eqtri 95 . . . . . . . . 9 |- [x:al = z:al] |= [A = (\x:al Az:al)]
363, 5, 2, 35oveq1 99 . . . . . . . 8 |- [x:al = z:al] |= [[A ==> T] = [(\x:al Az:al) ==> T]]
373, 10, 26, 36oveq2 101 . . . . . . 7 |- [x:al = z:al] |= [[R ==> [A ==> T]] = [R ==> [(\x:al Az:al) ==> T]]]
387, 12, 16, 25, 37insti 114 . . . . . 6 |- T. |= [R ==> [(\x:al Az:al) ==> T]]
3910, 38a1i 28 . . . . 5 |- R |= [R ==> [(\x:al Az:al) ==> T]]
409, 11, 39mpd 156 . . . 4 |- R |= [(\x:al Az:al) ==> T]
4140alrimiv 151 . . 3 |- R |= (A.\z:al [(\x:al Az:al) ==> T])
42 wex 139 . . . 4 |- E.:((al -> *) -> *)
4342, 6wc 50 . . 3 |- (E.\x:al A):*
4441, 43adantr 55 . 2 |- (R, (E.\x:al A)) |= (A.\z:al [(\x:al Az:al) ==> T])
4510, 43simpr 23 . . . 4 |- (R, (E.\x:al A)) |= (E.\x:al A)
4644ax-cb1 29 . . . . 5 |- (R, (E.\x:al A)):*
476exval 143 . . . . 5 |- T. |= [(E.\x:al A) = (A.\y:* [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*])]
4846, 47a1i 28 . . . 4 |- (R, (E.\x:al A)) |= [(E.\x:al A) = (A.\y:* [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*])]
4945, 48mpbi 82 . . 3 |- (R, (E.\x:al A)) |= (A.\y:* [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*])
50 wal 134 . . . . . 6 |- A.:((al -> *) -> *)
51 wv 64 . . . . . . . 8 |- y:*:*
523, 8, 51wov 72 . . . . . . 7 |- [(\x:al Az:al) ==> y:*]:*
5352wl 66 . . . . . 6 |- \z:al [(\x:al Az:al) ==> y:*]:(al -> *)
5450, 53wc 50 . . . . 5 |- (A.\z:al [(\x:al Az:al) ==> y:*]):*
553, 54, 51wov 72 . . . 4 |- [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*]:*
5651, 2weqi 76 . . . . . . . . 9 |- [y:* = T]:*
5756id 25 . . . . . . . 8 |- [y:* = T] |= [y:* = T]
583, 8, 51, 57oveq2 101 . . . . . . 7 |- [y:* = T] |= [[(\x:al Az:al) ==> y:*] = [(\x:al Az:al) ==> T]]
5952, 58leq 91 . . . . . 6 |- [y:* = T] |= [\z:al [(\x:al Az:al) ==> y:*] = \z:al [(\x:al Az:al) ==> T]]
6050, 53, 59ceq2 90 . . . . 5 |- [y:* = T] |= [(A.\z:al [(\x:al Az:al) ==> y:*]) = (A.\z:al [(\x:al Az:al) ==> T])]
613, 54, 51, 60, 57oveq12 100 . . . 4 |- [y:* = T] |= [[(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*] = [(A.\z:al [(\x:al Az:al) ==> T]) ==> T]]
6255, 2, 61cla4v 152 . . 3 |- (A.\y:* [(A.\z:al [(\x:al Az:al) ==> y:*]) ==> y:*]) |= [(A.\z:al [(\x:al Az:al) ==> T]) ==> T]
6349, 62syl 16 . 2 |- (R, (E.\x:al A)) |= [(A.\z:al [(\x:al Az:al) ==> T]) ==> T]
642, 44, 63mpd 156 1 |- (R, (E.\x:al A)) |= T
Colors of variables: type var term
Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9  kct 10   |= wffMMJ2 11   ==> 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:  eximdv  185  alnex  186
  Copyright terms: Public domain W3C validator