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

Theorem ax11 214
Description: Axiom of Variable Substitution. It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. (Contributed by Mario Carneiro, 10-Oct-2014.)
Hypothesis
Ref Expression
ax11.1 |- A:*
Assertion
Ref Expression
ax11 |- T. |= [[x:al = y:al] ==> [(A.\y:al A) ==> (A.\x:al [[x:al = y:al] ==> A])]]
Distinct variable groups:   x,A   x,y,al

Proof of Theorem ax11
StepHypRef Expression
1 wal 134 . . . . . . . 8 |- A.:((al -> *) -> *)
2 ax11.1 . . . . . . . . 9 |- A:*
32wl 66 . . . . . . . 8 |- \y:al A:(al -> *)
41, 3wc 50 . . . . . . 7 |- (A.\y:al A):*
54id 25 . . . . . 6 |- (A.\y:al A) |= (A.\y:al A)
6 wv 64 . . . . . . . . . 10 |- x:al:al
73, 6wc 50 . . . . . . . . 9 |- (\y:al Ax:al):*
87wl 66 . . . . . . . 8 |- \x:al (\y:al Ax:al):(al -> *)
93eta 178 . . . . . . . 8 |- T. |= [\x:al (\y:al Ax:al) = \y:al A]
101, 8, 9ceq2 90 . . . . . . 7 |- T. |= [(A.\x:al (\y:al Ax:al)) = (A.\y:al A)]
114, 10a1i 28 . . . . . 6 |- (A.\y:al A) |= [(A.\x:al (\y:al Ax:al)) = (A.\y:al A)]
125, 11mpbir 87 . . . . 5 |- (A.\y:al A) |= (A.\x:al (\y:al Ax:al))
13 wim 137 . . . . . . . . 9 |- ==> :(* -> (* -> *))
14 wv 64 . . . . . . . . . 10 |- y:al:al
156, 14weqi 76 . . . . . . . . 9 |- [x:al = y:al]:*
1613, 15, 2wov 72 . . . . . . . 8 |- [[x:al = y:al] ==> A]:*
1716wl 66 . . . . . . 7 |- \x:al [[x:al = y:al] ==> A]:(al -> *)
181, 17wc 50 . . . . . 6 |- (A.\x:al [[x:al = y:al] ==> A]):*
191, 8wc 50 . . . . . . 7 |- (A.\x:al (\y:al Ax:al)):*
2019id 25 . . . . . 6 |- (A.\x:al (\y:al Ax:al)) |= (A.\x:al (\y:al Ax:al))
2115, 4simpr 23 . . . . . . . . . . 11 |- ([x:al = y:al], (A.\y:al A)) |= (A.\y:al A)
2221ax-cb1 29 . . . . . . . . . . . 12 |- ([x:al = y:al], (A.\y:al A)):*
2322, 10a1i 28 . . . . . . . . . . 11 |- ([x:al = y:al], (A.\y:al A)) |= [(A.\x:al (\y:al Ax:al)) = (A.\y:al A)]
2421, 23mpbir 87 . . . . . . . . . 10 |- ([x:al = y:al], (A.\y:al A)) |= (A.\x:al (\y:al Ax:al))
2524ax-cb2 30 . . . . . . . . 9 |- (A.\x:al (\y:al Ax:al)):*
2613, 25, 18wov 72 . . . . . . . 8 |- [(A.\x:al (\y:al Ax:al)) ==> (A.\x:al [[x:al = y:al] ==> A])]:*
277, 15simpl 22 . . . . . . . . . . . . 13 |- ((\y:al Ax:al), [x:al = y:al]) |= (\y:al Ax:al)
287, 15simpr 23 . . . . . . . . . . . . . . 15 |- ((\y:al Ax:al), [x:al = y:al]) |= [x:al = y:al]
293, 6, 28ceq2 90 . . . . . . . . . . . . . 14 |- ((\y:al Ax:al), [x:al = y:al]) |= [(\y:al Ax:al) = (\y:al Ay:al)]
307, 15wct 48 . . . . . . . . . . . . . . 15 |- ((\y:al Ax:al), [x:al = y:al]):*
312beta 92 . . . . . . . . . . . . . . 15 |- T. |= [(\y:al Ay:al) = A]
3230, 31a1i 28 . . . . . . . . . . . . . 14 |- ((\y:al Ax:al), [x:al = y:al]) |= [(\y:al Ay:al) = A]
337, 29, 32eqtri 95 . . . . . . . . . . . . 13 |- ((\y:al Ax:al), [x:al = y:al]) |= [(\y:al Ax:al) = A]
3427, 33mpbi 82 . . . . . . . . . . . 12 |- ((\y:al Ax:al), [x:al = y:al]) |= A
3534ex 158 . . . . . . . . . . 11 |- (\y:al Ax:al) |= [[x:al = y:al] ==> A]
36 wtru 43 . . . . . . . . . . 11 |- T.:*
3735, 36adantl 56 . . . . . . . . . 10 |- (T., (\y:al Ax:al)) |= [[x:al = y:al] ==> A]
3837ex 158 . . . . . . . . 9 |- T. |= [(\y:al Ax:al) ==> [[x:al = y:al] ==> A]]
3938alrimiv 151 . . . . . . . 8 |- T. |= (A.\x:al [(\y:al Ax:al) ==> [[x:al = y:al] ==> A]])
407, 16ax5 207 . . . . . . . 8 |- T. |= [(A.\x:al [(\y:al Ax:al) ==> [[x:al = y:al] ==> A]]) ==> [(A.\x:al (\y:al Ax:al)) ==> (A.\x:al [[x:al = y:al] ==> A])]]
4126, 39, 40mpd 156 . . . . . . 7 |- T. |= [(A.\x:al (\y:al Ax:al)) ==> (A.\x:al [[x:al = y:al] ==> A])]
4219, 41a1i 28 . . . . . 6 |- (A.\x:al (\y:al Ax:al)) |= [(A.\x:al (\y:al Ax:al)) ==> (A.\x:al [[x:al = y:al] ==> A])]
4318, 20, 42mpd 156 . . . . 5 |- (A.\x:al (\y:al Ax:al)) |= (A.\x:al [[x:al = y:al] ==> A])
4412, 43syl 16 . . . 4 |- (A.\y:al A) |= (A.\x:al [[x:al = y:al] ==> A])
4536, 15wct 48 . . . 4 |- (T., [x:al = y:al]):*
4644, 45adantl 56 . . 3 |- ((T., [x:al = y:al]), (A.\y:al A)) |= (A.\x:al [[x:al = y:al] ==> A])
4746ex 158 . 2 |- (T., [x:al = y:al]) |= [(A.\y:al A) ==> (A.\x:al [[x:al = y:al] ==> A])]
4847ex 158 1 |- T. |= [[x:al = y:al] ==> [(A.\y:al A) ==> (A.\x:al [[x:al = y:al] ==> A])]]
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  wffMMJ2t 12   ==> tim 121  A.tal 122
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  ax-eta 177
This theorem depends on definitions:  df-ov 73  df-al 126  df-an 128  df-im 129
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator