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	|- T. |= [[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] |= T.
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 |- T. |= [[A /\ B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
15	4, 14	a1i 28	. . . . . . 7 |- [A /\ B] |= [[A /\ B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
16	13, 15	mpbi 82	. . . . . 6 |- [A /\ B] |= [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]
17	8, 11, 16	ceq1 89	. . . . 5 |- [A /\ B] |= [(\f:(* -> (* -> *)) [Af:(* -> (* -> *))B]\x:* \y:* x:*) = (\f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]\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 |- T. |= [[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 |- T. |= [(\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 |- T.:*
32	6, 31, 31	wov 72	. . . . . . 7 |- [T.f:(* -> (* -> *))T.]:*
33	6, 31, 31, 19	oveq 102	. . . . . . . 8 |- [f:(* -> (* -> *)) = \x:* \y:* x:*] |= [[T.f:(* -> (* -> *))T.] = [T.\x:* \y:* x:*T.]]
34	9, 31	weqi 76	. . . . . . . . . . 11 |- [x:* = T.]:*
35	34	id 25	. . . . . . . . . 10 |- [x:* = T.] |= [x:* = T.]
36	23, 31	weqi 76	. . . . . . . . . . 11 |- [y:* = T.]:*
37	36, 31	eqid 83	. . . . . . . . . 10 |- [y:* = T.] |= [T. = T.]
38	9, 31, 31, 35, 37	ovl 117	. . . . . . . . 9 |- T. |= [[T.\x:* \y:* x:*T.] = T.]
39	18, 38	a1i 28	. . . . . . . 8 |- [f:(* -> (* -> *)) = \x:* \y:* x:*] |= [[T.\x:* \y:* x:*T.] = T.]
40	32, 33, 39	eqtri 95	. . . . . . 7 |- [f:(* -> (* -> *)) = \x:* \y:* x:*] |= [[T.f:(* -> (* -> *))T.] = T.]
41	32, 11, 40	cl 116	. . . . . 6 |- T. |= [(\f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]\x:* \y:* x:*) = T.]
42	4, 41	a1i 28	. . . . 5 |- [A /\ B] |= [(\f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]\x:* \y:* x:*) = T.]
43	12, 17, 30, 42	3eqtr3i 97	. . . 4 |- [A /\ B] |= [A = T.]
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:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]\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 |- T. |= [(\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 |- T. |= [[A\x:* \y:* y:*B] = B]
56	31, 55	a1i 28	. . . . . . 7 |- T. |= [[A\x:* \y:* y:*B] = B]
57	47, 52, 56	eqtri 95	. . . . . 6 |- T. |= [(\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:*] |= [[T.f:(* -> (* -> *))T.] = [T.\x:* \y:* y:*T.]]
60	34, 23	eqid 83	. . . . . . . . . 10 |- [x:* = T.] |= [y:* = y:*]
61	36	id 25	. . . . . . . . . 10 |- [y:* = T.] |= [y:* = T.]
62	23, 31, 31, 60, 61	ovl 117	. . . . . . . . 9 |- T. |= [[T.\x:* \y:* y:*T.] = T.]
63	49, 62	a1i 28	. . . . . . . 8 |- [f:(* -> (* -> *)) = \x:* \y:* y:*] |= [[T.\x:* \y:* y:*T.] = T.]
64	32, 59, 63	eqtri 95	. . . . . . 7 |- [f:(* -> (* -> *)) = \x:* \y:* y:*] |= [[T.f:(* -> (* -> *))T.] = T.]
65	32, 46, 64	cl 116	. . . . . 6 |- T. |= [(\f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]\x:* \y:* y:*) = T.]
66	4, 65	a1i 28	. . . . 5 |- [A /\ B] |= [(\f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]\x:* \y:* y:*) = T.]
67	47, 48, 58, 66	3eqtr3i 97	. . . 4 |- [A /\ B] |= [B = T.]
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) |= [T. = A]
72	2, 3	simpr 23	. . . . . . 7 |- (A, B) |= B
73	72	eqtru 86	. . . . . 6 |- (A, B) |= [T. = B]
74	6, 31, 31, 71, 73	oveq12 100	. . . . 5 |- (A, B) |= [[T.f:(* -> (* -> *))T.] = [Af:(* -> (* -> *))B]]
75	32, 74	eqcomi 79	. . . 4 |- (A, B) |= [[Af:(* -> (* -> *))B] = [T.f:(* -> (* -> *))T.]]
76	7, 75	leq 91	. . 3 |- (A, B) |= [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]
77	70	ax-cb1 29	. . . 4 |- (A, B):*
78	77, 14	a1i 28	. . 3 |- (A, B) |= [[A /\ B] = [\f:(* -> (* -> *)) [Af:(* -> (* -> *))B] = \f:(* -> (* -> *)) [T.f:(* -> (* -> *))T.]]]
79	76, 78	mpbir 87	. 2 |- (A, B) |= [A /\ B]
80	69, 79	dedi 85	1 |- T. |= [[A /\ B] = (A, B)]

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.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