Theorem alnex 186

Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by Mario Carneiro, 10-Oct-2014.)

Hypothesis

Ref	Expression
alnex1.1	⊢ A:∗

Assertion

Ref	Expression
alnex	⊢ ⊤⊧[(∀λx:α (¬ A)) = (¬ (∃λx:α A))]

Distinct variable group:   α,x

Proof of Theorem alnex

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		alnex1.1	. . . . . 6 ⊢ A:∗
2		wfal 135	. . . . . 6 ⊢ ⊥:∗
3		wnot 138	. . . . . . . . 9 ⊢ ¬ :(∗ → ∗)
4	3, 1	wc 50	. . . . . . . 8 ⊢ (¬ A):∗
5	4	ax4 150	. . . . . . 7 ⊢ (∀λx:α (¬ A))⊧(¬ A)
6	5	ax-cb1 29	. . . . . . . 8 ⊢ (∀λx:α (¬ A)):∗
7	1	notval 145	. . . . . . . 8 ⊢ ⊤⊧[(¬ A) = [A ⇒ ⊥]]
8	6, 7	a1i 28	. . . . . . 7 ⊢ (∀λx:α (¬ A))⊧[(¬ A) = [A ⇒ ⊥]]
9	5, 8	mpbi 82	. . . . . 6 ⊢ (∀λx:α (¬ A))⊧[A ⇒ ⊥]
10	1, 2, 9	imp 157	. . . . 5 ⊢ ((∀λx:α (¬ A)), A)⊧⊥
11		wal 134	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
12	4	wl 66	. . . . . 6 ⊢ λx:α (¬ A):(α → ∗)
13		wv 64	. . . . . 6 ⊢ y:α:α
14	11, 13	ax-17 105	. . . . . 6 ⊢ ⊤⊧[(λx:α ∀y:α) = ∀]
15	4, 13	ax-hbl1 103	. . . . . 6 ⊢ ⊤⊧[(λx:α λx:α (¬ A)y:α) = λx:α (¬ A)]
16	11, 12, 13, 14, 15	hbc 110	. . . . 5 ⊢ ⊤⊧[(λx:α (∀λx:α (¬ A))y:α) = (∀λx:α (¬ A))]
17	2, 13	ax-17 105	. . . . 5 ⊢ ⊤⊧[(λx:α ⊥y:α) = ⊥]
18	10, 16, 17	exlimd 183	. . . 4 ⊢ ((∀λx:α (¬ A)), (∃λx:α A))⊧⊥
19	18	ex 158	. . 3 ⊢ (∀λx:α (¬ A))⊧[(∃λx:α A) ⇒ ⊥]
20		wex 139	. . . . . 6 ⊢ ∃:((α → ∗) → ∗)
21	1	wl 66	. . . . . 6 ⊢ λx:α A:(α → ∗)
22	20, 21	wc 50	. . . . 5 ⊢ (∃λx:α A):∗
23	22	notval 145	. . . 4 ⊢ ⊤⊧[(¬ (∃λx:α A)) = [(∃λx:α A) ⇒ ⊥]]
24	6, 23	a1i 28	. . 3 ⊢ (∀λx:α (¬ A))⊧[(¬ (∃λx:α A)) = [(∃λx:α A) ⇒ ⊥]]
25	19, 24	mpbir 87	. 2 ⊢ (∀λx:α (¬ A))⊧(¬ (∃λx:α A))
26	1	19.8a 170	. . . . . 6 ⊢ A⊧(∃λx:α A)
27		wtru 43	. . . . . 6 ⊢ ⊤:∗
28	26, 27	adantl 56	. . . . 5 ⊢ (⊤, A)⊧(∃λx:α A)
29	28	con3d 162	. . . 4 ⊢ (⊤, (¬ (∃λx:α A)))⊧(¬ A)
30	29	trul 39	. . 3 ⊢ (¬ (∃λx:α A))⊧(¬ A)
31	3, 13	ax-17 105	. . . 4 ⊢ ⊤⊧[(λx:α ¬ y:α) = ¬ ]
32	20, 13	ax-17 105	. . . . 5 ⊢ ⊤⊧[(λx:α ∃y:α) = ∃]
33	1, 13	ax-hbl1 103	. . . . 5 ⊢ ⊤⊧[(λx:α λx:α Ay:α) = λx:α A]
34	20, 21, 13, 32, 33	hbc 110	. . . 4 ⊢ ⊤⊧[(λx:α (∃λx:α A)y:α) = (∃λx:α A)]
35	3, 22, 13, 31, 34	hbc 110	. . 3 ⊢ ⊤⊧[(λx:α (¬ (∃λx:α A))y:α) = (¬ (∃λx:α A))]
36	30, 35	alrimi 182	. 2 ⊢ (¬ (∃λx:α A))⊧(∀λx:α (¬ A))
37	25, 36	dedi 85	1 ⊢ ⊤⊧[(∀λx:α (¬ A)) = (¬ (∃λx:α A))]

This proof depends on syntax axioms:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11  wffMMJ2t 12  ⊥tfal 118  ¬ tne 120   ⇒ tim 121  ∀tal 122  ∃tex 123

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-fal 127  df-an 128  df-im 129  df-not 130  df-ex 131

This theorem is used by:  exnal1  187  exnal  201  ax9  212