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

Theorem ax7 209
Description: Axiom of Quantifier Commutation. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). (Contributed by Mario Carneiro, 10-Oct-2014.)
Hypothesis
Ref Expression
ax7.1 R:∗
Assertion
Ref Expression
ax7 ⊤⊧[(λx:α (λy:α R)) ⇒ (λy:α (λx:α R))]
Distinct variable group:   x,y,α

Proof of Theorem ax7
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 wal 134 . . . . . . . 8 :((α → ∗) → ∗)
2 ax7.1 . . . . . . . . 9 R:∗
32wl 66 . . . . . . . 8 λy:α R:(α → ∗)
41, 3wc 50 . . . . . . 7 (λy:α R):∗
54ax4 150 . . . . . 6 (λx:α (λy:α R))⊧(λy:α R)
62ax4 150 . . . . . 6 (λy:α R)⊧R
75, 6syl 16 . . . . 5 (λx:α (λy:α R))⊧R
84wl 66 . . . . . 6 λx:α (λy:α R):(α → ∗)
9 wv 64 . . . . . 6 z:α:α
101, 9ax-17 105 . . . . . 6 ⊤⊧[(λx:α z:α) = ]
114, 9ax-hbl1 103 . . . . . 6 ⊤⊧[(λx:α λx:α (λy:α R)z:α) = λx:α (λy:α R)]
121, 8, 9, 10, 11hbc 110 . . . . 5 ⊤⊧[(λx:α (λx:α (λy:α R))z:α) = (λx:α (λy:α R))]
137, 12alrimi 182 . . . 4 (λx:α (λy:α R))⊧(λx:α R)
141, 9ax-17 105 . . . . 5 ⊤⊧[(λy:α z:α) = ]
152, 9ax-hbl1 103 . . . . . . 7 ⊤⊧[(λy:α λy:α Rz:α) = λy:α R]
161, 3, 9, 14, 15hbc 110 . . . . . 6 ⊤⊧[(λy:α (λy:α R)z:α) = (λy:α R)]
174, 9, 16hbl 112 . . . . 5 ⊤⊧[(λy:α λx:α (λy:α R)z:α) = λx:α (λy:α R)]
181, 8, 9, 14, 17hbc 110 . . . 4 ⊤⊧[(λy:α (λx:α (λy:α R))z:α) = (λx:α (λy:α R))]
1913, 18alrimi 182 . . 3 (λx:α (λy:α R))⊧(λy:α (λx:α R))
20 wtru 43 . . 3 ⊤:∗
2119, 20adantl 56 . 2 (⊤, (λx:α (λy:α R)))⊧(λy:α (λx:α R))
2221ex 158 1 ⊤⊧[(λx:α (λy:α R)) ⇒ (λy:α (λx:α R))]
Colors of variables: type var term
Syntax hints:  tv 1  ht 2  hb 3  kc 5  λkl 6  kt 8  [kbr 9  wffMMJ2 11  wffMMJ2t 12  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