Theorem ax10 200

Description: Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).

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.

Step	Hyp	Ref	Expression
1		wv 58	. . . . . 6 ⊢ z:α:α
2		wv 58	. . . . . . . 8 ⊢ x:α:α
3		wv 58	. . . . . . . 8 ⊢ y:α:α
4	2, 3	weqi 68	. . . . . . 7 ⊢ [x:α = y:α]:∗
5		weq 38	. . . . . . . 8 ⊢ = :(α → (α → ∗))
6	5, 2, 1	wov 64	. . . . . . . . 9 ⊢ [x:α = z:α]:∗
7	6	id 25	. . . . . . . 8 ⊢ [x:α = z:α]⊧[x:α = z:α]
8	5, 2, 3, 7	oveq1 89	. . . . . . 7 ⊢ [x:α = z:α]⊧[[x:α = y:α] = [z:α = y:α]]
9	4, 1, 8	cla4v 142	. . . . . 6 ⊢ (∀λx:α [x:α = y:α])⊧[z:α = y:α]
10	4	ax4 140	. . . . . . 7 ⊢ (∀λx:α [x:α = y:α])⊧[x:α = y:α]
11	2, 10	eqcomi 70	. . . . . 6 ⊢ (∀λx:α [x:α = y:α])⊧[y:α = x:α]
12	1, 9, 11	eqtri 85	. . . . 5 ⊢ (∀λx:α [x:α = y:α])⊧[z:α = x:α]
13	12	alrimiv 141	. . . 4 ⊢ (∀λx:α [x:α = y:α])⊧(∀λz:α [z:α = x:α])
14		wal 124	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
15	4	wl 59	. . . . . 6 ⊢ λx:α [x:α = y:α]:(α → ∗)
16	14, 15	wc 45	. . . . 5 ⊢ (∀λx:α [x:α = y:α]):∗
17	3, 2	weqi 68	. . . . . . 7 ⊢ [y:α = x:α]:∗
18	17	wl 59	. . . . . 6 ⊢ λy:α [y:α = x:α]:(α → ∗)
19	3, 1	weqi 68	. . . . . . . . 9 ⊢ [y:α = z:α]:∗
20	19	id 25	. . . . . . . 8 ⊢ [y:α = z:α]⊧[y:α = z:α]
21	5, 3, 2, 20	oveq1 89	. . . . . . 7 ⊢ [y:α = z:α]⊧[[y:α = x:α] = [z:α = x:α]]
22	17, 21	cbv 168	. . . . . 6 ⊢ ⊤⊧[λy:α [y:α = x:α] = λz:α [z:α = x:α]]
23	14, 18, 22	ceq2 80	. . . . 5 ⊢ ⊤⊧[(∀λy:α [y:α = x:α]) = (∀λz:α [z:α = x:α])]
24	16, 23	a1i 28	. . . 4 ⊢ (∀λx:α [x:α = y:α])⊧[(∀λy:α [y:α = x:α]) = (∀λz:α [z:α = x:α])]
25	13, 24	mpbir 77	. . 3 ⊢ (∀λx:α [x:α = y:α])⊧(∀λy:α [y:α = x:α])
26		wtru 40	. . 3 ⊢ ⊤:∗
27	25, 26	adantl 51	. 2 ⊢ (⊤, (∀λx:α [x:α = y:α]))⊧(∀λy:α [y:α = x:α])
28	27	ex 148	1 ⊢ ⊤⊧[(∀λx:α [x:α = y:α]) ⇒ (∀λy:α [y:α = x:α])]

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11   ⇒ tim 111  ∀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)