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

Theorem ax10 213
 Description: Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by Mario Carneiro, 10-Oct-2014.)
Assertion
Ref Expression
ax10 ⊤⊧[(λx:α [x:α = y:α]) ⇒ (λy:α [y:α = x:α])]
Distinct variable group:   x,y,α

Proof of Theorem ax10
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 wv 64 . . . . . 6 z:α:α
2 wv 64 . . . . . . . 8 x:α:α
3 wv 64 . . . . . . . 8 y:α:α
42, 3weqi 76 . . . . . . 7 [x:α = y:α]:∗
5 weq 41 . . . . . . . 8 = :(α → (α → ∗))
65, 2, 1wov 72 . . . . . . . . 9 [x:α = z:α]:∗
76id 25 . . . . . . . 8 [x:α = z:α]⊧[x:α = z:α]
85, 2, 3, 7oveq1 99 . . . . . . 7 [x:α = z:α]⊧[[x:α = y:α] = [z:α = y:α]]
94, 1, 8cla4v 152 . . . . . 6 (λx:α [x:α = y:α])⊧[z:α = y:α]
104ax4 150 . . . . . . 7 (λx:α [x:α = y:α])⊧[x:α = y:α]
112, 10eqcomi 79 . . . . . 6 (λx:α [x:α = y:α])⊧[y:α = x:α]
121, 9, 11eqtri 95 . . . . 5 (λx:α [x:α = y:α])⊧[z:α = x:α]
1312alrimiv 151 . . . 4 (λx:α [x:α = y:α])⊧(λz:α [z:α = x:α])
14 wal 134 . . . . . 6 :((α → ∗) → ∗)
154wl 66 . . . . . 6 λx:α [x:α = y:α]:(α → ∗)
1614, 15wc 50 . . . . 5 (λx:α [x:α = y:α]):∗
173, 2weqi 76 . . . . . . 7 [y:α = x:α]:∗
1817wl 66 . . . . . 6 λy:α [y:α = x:α]:(α → ∗)
193, 1weqi 76 . . . . . . . . 9 [y:α = z:α]:∗
2019id 25 . . . . . . . 8 [y:α = z:α]⊧[y:α = z:α]
215, 3, 2, 20oveq1 99 . . . . . . 7 [y:α = z:α]⊧[[y:α = x:α] = [z:α = x:α]]
2217, 21cbv 180 . . . . . 6 ⊤⊧[λy:α [y:α = x:α] = λz:α [z:α = x:α]]
2314, 18, 22ceq2 90 . . . . 5 ⊤⊧[(λy:α [y:α = x:α]) = (λz:α [z:α = x:α])]
2416, 23a1i 28 . . . 4 (λx:α [x:α = y:α])⊧[(λy:α [y:α = x:α]) = (λz:α [z:α = x:α])]
2513, 24mpbir 87 . . 3 (λx:α [x:α = y:α])⊧(λy:α [y:α = x:α])
26 wtru 43 . . 3 ⊤:∗
2725, 26adantl 56 . 2 (⊤, (λx:α [x:α = y:α]))⊧(λy:α [y:α = x:α])
2827ex 158 1 ⊤⊧[(λx:α [x:α = y:α]) ⇒ (λy:α [y:α = x:α])]
 Colors of variables: type var term Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11   ⇒ tim 121  ∀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