Theorem dfan2 154

Description: An alternative definition of the "and" term in terms of the context conjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Hypotheses

Ref	Expression
dfan2.1	⊢ A:∗
dfan2.2	⊢ B:∗

Assertion

Ref	Expression
dfan2	⊢ ⊤⊧[[A ∧ B] = (A, B)]

Proof of Theorem dfan2

Dummy variables x f y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wan 136	. . . . . 6 ⊢ ∧ :(∗ → (∗ → ∗))
2		dfan2.1	. . . . . 6 ⊢ A:∗
3		dfan2.2	. . . . . 6 ⊢ B:∗
4	1, 2, 3	wov 72	. . . . 5 ⊢ [A ∧ B]:∗
5	4	trud 27	. . . 4 ⊢ [A ∧ B]⊧⊤
6		wv 64	. . . . . . . 8 ⊢ f:(∗ → (∗ → ∗)):(∗ → (∗ → ∗))
7	6, 2, 3	wov 72	. . . . . . 7 ⊢ [Af:(∗ → (∗ → ∗))B]:∗
8	7	wl 66	. . . . . 6 ⊢ λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]:((∗ → (∗ → ∗)) → ∗)
9		wv 64	. . . . . . . 8 ⊢ x:∗:∗
10	9	wl 66	. . . . . . 7 ⊢ λy:∗ x:∗:(∗ → ∗)
11	10	wl 66	. . . . . 6 ⊢ λx:∗ λy:∗ x:∗:(∗ → (∗ → ∗))
12	8, 11	wc 50	. . . . 5 ⊢ (λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ x:∗):∗
13	4	id 25	. . . . . . 7 ⊢ [A ∧ B]⊧[A ∧ B]
14	2, 3	anval 148	. . . . . . . 8 ⊢ ⊤⊧[[A ∧ B] = [λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
15	4, 14	a1i 28	. . . . . . 7 ⊢ [A ∧ B]⊧[[A ∧ B] = [λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
16	13, 15	mpbi 82	. . . . . 6 ⊢ [A ∧ B]⊧[λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
17	8, 11, 16	ceq1 89	. . . . 5 ⊢ [A ∧ B]⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ x:∗) = (λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ x:∗)]
18	6, 11	weqi 76	. . . . . . . . . 10 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]:∗
19	18	id 25	. . . . . . . . 9 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]
20	6, 2, 3, 19	oveq 102	. . . . . . . 8 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[Af:(∗ → (∗ → ∗))B] = [Aλx:∗ λy:∗ x:∗B]]
21	9, 2	weqi 76	. . . . . . . . . . 11 ⊢ [x:∗ = A]:∗
22	21	id 25	. . . . . . . . . 10 ⊢ [x:∗ = A]⊧[x:∗ = A]
23		wv 64	. . . . . . . . . . . 12 ⊢ y:∗:∗
24	23, 3	weqi 76	. . . . . . . . . . 11 ⊢ [y:∗ = B]:∗
25	24, 2	eqid 83	. . . . . . . . . 10 ⊢ [y:∗ = B]⊧[A = A]
26	9, 2, 3, 22, 25	ovl 117	. . . . . . . . 9 ⊢ ⊤⊧[[Aλx:∗ λy:∗ x:∗B] = A]
27	18, 26	a1i 28	. . . . . . . 8 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[Aλx:∗ λy:∗ x:∗B] = A]
28	7, 20, 27	eqtri 95	. . . . . . 7 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[Af:(∗ → (∗ → ∗))B] = A]
29	7, 11, 28	cl 116	. . . . . 6 ⊢ ⊤⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ x:∗) = A]
30	4, 29	a1i 28	. . . . 5 ⊢ [A ∧ B]⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ x:∗) = A]
31		wtru 43	. . . . . . . 8 ⊢ ⊤:∗
32	6, 31, 31	wov 72	. . . . . . 7 ⊢ [⊤f:(∗ → (∗ → ∗))⊤]:∗
33	6, 31, 31, 19	oveq 102	. . . . . . . 8 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[⊤f:(∗ → (∗ → ∗))⊤] = [⊤λx:∗ λy:∗ x:∗⊤]]
34	9, 31	weqi 76	. . . . . . . . . . 11 ⊢ [x:∗ = ⊤]:∗
35	34	id 25	. . . . . . . . . 10 ⊢ [x:∗ = ⊤]⊧[x:∗ = ⊤]
36	23, 31	weqi 76	. . . . . . . . . . 11 ⊢ [y:∗ = ⊤]:∗
37	36, 31	eqid 83	. . . . . . . . . 10 ⊢ [y:∗ = ⊤]⊧[⊤ = ⊤]
38	9, 31, 31, 35, 37	ovl 117	. . . . . . . . 9 ⊢ ⊤⊧[[⊤λx:∗ λy:∗ x:∗⊤] = ⊤]
39	18, 38	a1i 28	. . . . . . . 8 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[⊤λx:∗ λy:∗ x:∗⊤] = ⊤]
40	32, 33, 39	eqtri 95	. . . . . . 7 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[⊤f:(∗ → (∗ → ∗))⊤] = ⊤]
41	32, 11, 40	cl 116	. . . . . 6 ⊢ ⊤⊧[(λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ x:∗) = ⊤]
42	4, 41	a1i 28	. . . . 5 ⊢ [A ∧ B]⊧[(λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ x:∗) = ⊤]
43	12, 17, 30, 42	3eqtr3i 97	. . . 4 ⊢ [A ∧ B]⊧[A = ⊤]
44	5, 43	mpbir 87	. . 3 ⊢ [A ∧ B]⊧A
45	23	wl 66	. . . . . . 7 ⊢ λy:∗ y:∗:(∗ → ∗)
46	45	wl 66	. . . . . 6 ⊢ λx:∗ λy:∗ y:∗:(∗ → (∗ → ∗))
47	8, 46	wc 50	. . . . 5 ⊢ (λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗):∗
48	8, 46, 16	ceq1 89	. . . . 5 ⊢ [A ∧ B]⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗) = (λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ y:∗)]
49	6, 46	weqi 76	. . . . . . . . . 10 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]:∗
50	49	id 25	. . . . . . . . 9 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]
51	6, 2, 3, 50	oveq 102	. . . . . . . 8 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[[Af:(∗ → (∗ → ∗))B] = [Aλx:∗ λy:∗ y:∗B]]
52	7, 46, 51	cl 116	. . . . . . 7 ⊢ ⊤⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗) = [Aλx:∗ λy:∗ y:∗B]]
53	21, 23	eqid 83	. . . . . . . . 9 ⊢ [x:∗ = A]⊧[y:∗ = y:∗]
54	24	id 25	. . . . . . . . 9 ⊢ [y:∗ = B]⊧[y:∗ = B]
55	23, 2, 3, 53, 54	ovl 117	. . . . . . . 8 ⊢ ⊤⊧[[Aλx:∗ λy:∗ y:∗B] = B]
56	31, 55	a1i 28	. . . . . . 7 ⊢ ⊤⊧[[Aλx:∗ λy:∗ y:∗B] = B]
57	47, 52, 56	eqtri 95	. . . . . 6 ⊢ ⊤⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗) = B]
58	4, 57	a1i 28	. . . . 5 ⊢ [A ∧ B]⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗) = B]
59	6, 31, 31, 50	oveq 102	. . . . . . . 8 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[[⊤f:(∗ → (∗ → ∗))⊤] = [⊤λx:∗ λy:∗ y:∗⊤]]
60	34, 23	eqid 83	. . . . . . . . . 10 ⊢ [x:∗ = ⊤]⊧[y:∗ = y:∗]
61	36	id 25	. . . . . . . . . 10 ⊢ [y:∗ = ⊤]⊧[y:∗ = ⊤]
62	23, 31, 31, 60, 61	ovl 117	. . . . . . . . 9 ⊢ ⊤⊧[[⊤λx:∗ λy:∗ y:∗⊤] = ⊤]
63	49, 62	a1i 28	. . . . . . . 8 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[[⊤λx:∗ λy:∗ y:∗⊤] = ⊤]
64	32, 59, 63	eqtri 95	. . . . . . 7 ⊢ [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[[⊤f:(∗ → (∗ → ∗))⊤] = ⊤]
65	32, 46, 64	cl 116	. . . . . 6 ⊢ ⊤⊧[(λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ y:∗) = ⊤]
66	4, 65	a1i 28	. . . . 5 ⊢ [A ∧ B]⊧[(λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ y:∗) = ⊤]
67	47, 48, 58, 66	3eqtr3i 97	. . . 4 ⊢ [A ∧ B]⊧[B = ⊤]
68	5, 67	mpbir 87	. . 3 ⊢ [A ∧ B]⊧B
69	44, 68	jca 18	. 2 ⊢ [A ∧ B]⊧(A, B)
70	2, 3	simpl 22	. . . . . . 7 ⊢ (A, B)⊧A
71	70	eqtru 86	. . . . . 6 ⊢ (A, B)⊧[⊤ = A]
72	2, 3	simpr 23	. . . . . . 7 ⊢ (A, B)⊧B
73	72	eqtru 86	. . . . . 6 ⊢ (A, B)⊧[⊤ = B]
74	6, 31, 31, 71, 73	oveq12 100	. . . . 5 ⊢ (A, B)⊧[[⊤f:(∗ → (∗ → ∗))⊤] = [Af:(∗ → (∗ → ∗))B]]
75	32, 74	eqcomi 79	. . . 4 ⊢ (A, B)⊧[[Af:(∗ → (∗ → ∗))B] = [⊤f:(∗ → (∗ → ∗))⊤]]
76	7, 75	leq 91	. . 3 ⊢ (A, B)⊧[λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
77	70	ax-cb1 29	. . . 4 ⊢ (A, B):∗
78	77, 14	a1i 28	. . 3 ⊢ (A, B)⊧[[A ∧ B] = [λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
79	76, 78	mpbir 87	. 2 ⊢ (A, B)⊧[A ∧ B]
80	69, 79	dedi 85	1 ⊢ ⊤⊧[[A ∧ B] = (A, B)]

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  kct 10  ⊧wffMMJ2 11  wffMMJ2t 12   ∧ tan 119

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

This theorem depends on definitions:  df-ov 73  df-an 128

This theorem is referenced by:  hbct  155  mpd  156  ex  158