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

Theorem ax11 201
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.
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 124 . . . . . . . 8 |- A.:((al -> *) -> *)
2 ax11.1 . . . . . . . . 9 |- A:*
32wl 59 . . . . . . . 8 |- \y:al A:(al -> *)
41, 3wc 45 . . . . . . 7 |- (A.\y:al A):*
54id 25 . . . . . 6 |- (A.\y:al A) |= (A.\y:al A)
6 wv 58 . . . . . . . . . 10 |- x:al:al
73, 6wc 45 . . . . . . . . 9 |- (\y:al Ax:al):*
87wl 59 . . . . . . . 8 |- \x:al (\y:al Ax:al):(al -> *)
93eta 166 . . . . . . . 8 |- T. |= [\x:al (\y:al Ax:al) = \y:al A]
101, 8, 9ceq2 80 . . . . . . 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 77 . . . . 5 |- (A.\y:al A) |= (A.\x:al (\y:al Ax:al))
13 wim 127 . . . . . . . . 9 |- ==> :(* -> (* -> *))
14 wv 58 . . . . . . . . . 10 |- y:al:al
156, 14weqi 68 . . . . . . . . 9 |- [x:al = y:al]:*
1613, 15, 2wov 64 . . . . . . . 8 |- [[x:al = y:al] ==> A]:*
1716wl 59 . . . . . . 7 |- \x:al [[x:al = y:al] ==> A]:(al -> *)
181, 17wc 45 . . . . . 6 |- (A.\x:al [[x:al = y:al] ==> A]):*
191, 8wc 45 . . . . . . 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 77 . . . . . . . . . 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 64 . . . . . . . 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 80 . . . . . . . . . . . . . 14 |- ((\y:al Ax:al), [x:al = y:al]) |= [(\y:al Ax:al) = (\y:al Ay:al)]
307, 15wct 44 . . . . . . . . . . . . . . 15 |- ((\y:al Ax:al), [x:al = y:al]):*
312beta 82 . . . . . . . . . . . . . . 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 85 . . . . . . . . . . . . 13 |- ((\y:al Ax:al), [x:al = y:al]) |= [(\y:al Ax:al) = A]
3427, 33mpbi 72 . . . . . . . . . . . 12 |- ((\y:al Ax:al), [x:al = y:al]) |= A
3534ex 148 . . . . . . . . . . 11 |- (\y:al Ax:al) |= [[x:al = y:al] ==> A]
36 wtru 40 . . . . . . . . . . 11 |- T.:*
3735, 36adantl 51 . . . . . . . . . 10 |- (T., (\y:al Ax:al)) |= [[x:al = y:al] ==> A]
3837ex 148 . . . . . . . . 9 |- T. |= [(\y:al Ax:al) ==> [[x:al = y:al] ==> A]]
3938alrimiv 141 . . . . . . . 8 |- T. |= (A.\x:al [(\y:al Ax:al) ==> [[x:al = y:al] ==> A]])
407, 16ax5 194 . . . . . . . 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 146 . . . . . . 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 146 . . . . 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 44 . . . 4 |- (T., [x:al = y:al]):*
4644, 45adantl 51 . . 3 |- ((T., [x:al = y:al]), (A.\y:al A)) |= (A.\x:al [[x:al = y:al] ==> A])
4746ex 148 . 2 |- (T., [x:al = y:al]) |= [(A.\y:al A) ==> (A.\x:al [[x:al = y:al] ==> A])]
4847ex 148 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 111  A.tal 112
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  ax-eta 165
This theorem depends on definitions:  df-ov 65  df-al 116  df-an 118  df-im 119
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator