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.

Step	Hyp	Ref	Expression
1		wv 64	. . . . . 6 ⊢ z:α:α
2		wv 64	. . . . . . . 8 ⊢ x:α:α
3		wv 64	. . . . . . . 8 ⊢ y:α:α
4	2, 3	weqi 76	. . . . . . 7 ⊢ [x:α = y:α]:∗
5		weq 41	. . . . . . . 8 ⊢ = :(α → (α → ∗))
6	5, 2, 1	wov 72	. . . . . . . . 9 ⊢ [x:α = z:α]:∗
7	6	id 25	. . . . . . . 8 ⊢ [x:α = z:α]⊧[x:α = z:α]
8	5, 2, 3, 7	oveq1 99	. . . . . . 7 ⊢ [x:α = z:α]⊧[[x:α = y:α] = [z:α = y:α]]
9	4, 1, 8	cla4v 152	. . . . . 6 ⊢ (∀λx:α [x:α = y:α])⊧[z:α = y:α]
10	4	ax4 150	. . . . . . 7 ⊢ (∀λx:α [x:α = y:α])⊧[x:α = y:α]
11	2, 10	eqcomi 79	. . . . . 6 ⊢ (∀λx:α [x:α = y:α])⊧[y:α = x:α]
12	1, 9, 11	eqtri 95	. . . . 5 ⊢ (∀λx:α [x:α = y:α])⊧[z:α = x:α]
13	12	alrimiv 151	. . . 4 ⊢ (∀λx:α [x:α = y:α])⊧(∀λz:α [z:α = x:α])
14		wal 134	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
15	4	wl 66	. . . . . 6 ⊢ λx:α [x:α = y:α]:(α → ∗)
16	14, 15	wc 50	. . . . 5 ⊢ (∀λx:α [x:α = y:α]):∗
17	3, 2	weqi 76	. . . . . . 7 ⊢ [y:α = x:α]:∗
18	17	wl 66	. . . . . 6 ⊢ λy:α [y:α = x:α]:(α → ∗)
19	3, 1	weqi 76	. . . . . . . . 9 ⊢ [y:α = z:α]:∗
20	19	id 25	. . . . . . . 8 ⊢ [y:α = z:α]⊧[y:α = z:α]
21	5, 3, 2, 20	oveq1 99	. . . . . . 7 ⊢ [y:α = z:α]⊧[[y:α = x:α] = [z:α = x:α]]
22	17, 21	cbv 180	. . . . . 6 ⊢ ⊤⊧[λy:α [y:α = x:α] = λz:α [z:α = x:α]]
23	14, 18, 22	ceq2 90	. . . . 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 87	. . 3 ⊢ (∀λx:α [x:α = y:α])⊧(∀λy:α [y:α = x:α])
26		wtru 43	. . 3 ⊢ ⊤:∗
27	25, 26	adantl 56	. 2 ⊢ (⊤, (∀λx:α [x:α = y:α]))⊧(∀λy:α [y:α = x:α])
28	27	ex 158	1 ⊢ ⊤⊧[(∀λx:α [x:α = y:α]) ⇒ (∀λy:α [y:α = x:α])]

This proof depends on syntax axioms:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11   ⇒ tim 121  ∀tal 122

This proof depends on 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 proof depends on definitions:  df-ov 73  df-al 126  df-an 128  df-im 129

This theorem is used by: (None)