Theorem alnex 174

Description: Theorem 19.7 of [Margaris] p. 89.

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 125	. . . . . 6 ⊢ ⊥:∗
3		wnot 128	. . . . . . . . 9 ⊢ ¬ :(∗ → ∗)
4	3, 1	wc 45	. . . . . . . 8 ⊢ (¬ A):∗
5	4	ax4 140	. . . . . . 7 ⊢ (∀λx:α (¬ A))⊧(¬ A)
6	5	ax-cb1 29	. . . . . . . 8 ⊢ (∀λx:α (¬ A)):∗
7	1	notval 135	. . . . . . . 8 ⊢ ⊤⊧[(¬ A) = [A ⇒ ⊥]]
8	6, 7	a1i 28	. . . . . . 7 ⊢ (∀λx:α (¬ A))⊧[(¬ A) = [A ⇒ ⊥]]
9	5, 8	mpbi 72	. . . . . 6 ⊢ (∀λx:α (¬ A))⊧[A ⇒ ⊥]
10	1, 2, 9	imp 147	. . . . 5 ⊢ ((∀λx:α (¬ A)), A)⊧⊥
11		wal 124	. . . . . 6 ⊢ ∀:((α → ∗) → ∗)
12	4	wl 59	. . . . . 6 ⊢ λx:α (¬ A):(α → ∗)
13		wv 58	. . . . . 6 ⊢ y:α:α
14	11, 13	ax-17 95	. . . . . 6 ⊢ ⊤⊧[(λx:α ∀y:α) = ∀]
15	4, 13	ax-hbl1 93	. . . . . 6 ⊢ ⊤⊧[(λx:α λx:α (¬ A)y:α) = λx:α (¬ A)]
16	11, 12, 13, 14, 15	hbc 100	. . . . 5 ⊢ ⊤⊧[(λx:α (∀λx:α (¬ A))y:α) = (∀λx:α (¬ A))]
17	2, 13	ax-17 95	. . . . 5 ⊢ ⊤⊧[(λx:α ⊥y:α) = ⊥]
18	10, 16, 17	exlimd 171	. . . 4 ⊢ ((∀λx:α (¬ A)), (∃λx:α A))⊧⊥
19	18	ex 148	. . 3 ⊢ (∀λx:α (¬ A))⊧[(∃λx:α A) ⇒ ⊥]
20		wex 129	. . . . . 6 ⊢ ∃:((α → ∗) → ∗)
21	1	wl 59	. . . . . 6 ⊢ λx:α A:(α → ∗)
22	20, 21	wc 45	. . . . 5 ⊢ (∃λx:α A):∗
23	22	notval 135	. . . 4 ⊢ ⊤⊧[(¬ (∃λx:α A)) = [(∃λx:α A) ⇒ ⊥]]
24	6, 23	a1i 28	. . 3 ⊢ (∀λx:α (¬ A))⊧[(¬ (∃λx:α A)) = [(∃λx:α A) ⇒ ⊥]]
25	19, 24	mpbir 77	. 2 ⊢ (∀λx:α (¬ A))⊧(¬ (∃λx:α A))
26	1	19.8a 160	. . . . . 6 ⊢ A⊧(∃λx:α A)
27		wtru 40	. . . . . 6 ⊢ ⊤:∗
28	26, 27	adantl 51	. . . . 5 ⊢ (⊤, A)⊧(∃λx:α A)
29	28	con3d 152	. . . 4 ⊢ (⊤, (¬ (∃λx:α A)))⊧(¬ A)
30	29	trul 37	. . 3 ⊢ (¬ (∃λx:α A))⊧(¬ A)
31	3, 13	ax-17 95	. . . 4 ⊢ ⊤⊧[(λx:α ¬ y:α) = ¬ ]
32	20, 13	ax-17 95	. . . . 5 ⊢ ⊤⊧[(λx:α ∃y:α) = ∃]
33	1, 13	ax-hbl1 93	. . . . 5 ⊢ ⊤⊧[(λx:α λx:α Ay:α) = λx:α A]
34	20, 21, 13, 32, 33	hbc 100	. . . 4 ⊢ ⊤⊧[(λx:α (∃λx:α A)y:α) = (∃λx:α A)]
35	3, 22, 13, 31, 34	hbc 100	. . 3 ⊢ ⊤⊧[(λx:α (¬ (∃λx:α A))y:α) = (¬ (∃λx:α A))]
36	30, 35	alrimi 170	. 2 ⊢ (¬ (∃λx:α A))⊧(∀λx:α (¬ A))
37	25, 36	dedi 75	1 ⊢ ⊤⊧[(∀λx:α (¬ A)) = (¬ (∃λx:α A))]

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11  wffMMJ2t 12  ⊥tfal 108  ¬ tne 110   ⇒ tim 111  ∀tal 112  ∃tex 113

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-fal 117  df-an 118  df-im 119  df-not 120  df-ex 121

This theorem is referenced by:  exnal1  175  exnal  188  ax9  199