Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  dfan2 GIF version

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.
StepHypRef Expression
1 wan 136 . . . . . 6 :(∗ → (∗ → ∗))
2 dfan2.1 . . . . . 6 A:∗
3 dfan2.2 . . . . . 6 B:∗
41, 2, 3wov 72 . . . . 5 [A B]:∗
54trud 27 . . . 4 [A B]⊧⊤
6 wv 64 . . . . . . . 8 f:(∗ → (∗ → ∗)):(∗ → (∗ → ∗))
76, 2, 3wov 72 . . . . . . 7 [Af:(∗ → (∗ → ∗))B]:∗
87wl 66 . . . . . 6 λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]:((∗ → (∗ → ∗)) → ∗)
9 wv 64 . . . . . . . 8 x:∗:∗
109wl 66 . . . . . . 7 λy:∗ x:∗:(∗ → ∗)
1110wl 66 . . . . . 6 λx:∗ λy:∗ x:∗:(∗ → (∗ → ∗))
128, 11wc 50 . . . . 5 (λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ x:∗):∗
134id 25 . . . . . . 7 [A B]⊧[A B]
142, 3anval 148 . . . . . . . 8 ⊤⊧[[A B] = [λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
154, 14a1i 28 . . . . . . 7 [A B]⊧[[A B] = [λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
1613, 15mpbi 82 . . . . . 6 [A B]⊧[λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
178, 11, 16ceq1 89 . . . . 5 [A B]⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ x:∗) = (λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ x:∗)]
186, 11weqi 76 . . . . . . . . . 10 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]:∗
1918id 25 . . . . . . . . 9 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]
206, 2, 3, 19oveq 102 . . . . . . . 8 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[Af:(∗ → (∗ → ∗))B] = [Aλx:∗ λy:∗ x:∗B]]
219, 2weqi 76 . . . . . . . . . . 11 [x:∗ = A]:∗
2221id 25 . . . . . . . . . 10 [x:∗ = A]⊧[x:∗ = A]
23 wv 64 . . . . . . . . . . . 12 y:∗:∗
2423, 3weqi 76 . . . . . . . . . . 11 [y:∗ = B]:∗
2524, 2eqid 83 . . . . . . . . . 10 [y:∗ = B]⊧[A = A]
269, 2, 3, 22, 25ovl 117 . . . . . . . . 9 ⊤⊧[[Aλx:∗ λy:∗ x:∗B] = A]
2718, 26a1i 28 . . . . . . . 8 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[Aλx:∗ λy:∗ x:∗B] = A]
287, 20, 27eqtri 95 . . . . . . 7 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[Af:(∗ → (∗ → ∗))B] = A]
297, 11, 28cl 116 . . . . . 6 ⊤⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ x:∗) = A]
304, 29a1i 28 . . . . 5 [A B]⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ x:∗) = A]
31 wtru 43 . . . . . . . 8 ⊤:∗
326, 31, 31wov 72 . . . . . . 7 [⊤f:(∗ → (∗ → ∗))⊤]:∗
336, 31, 31, 19oveq 102 . . . . . . . 8 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[⊤f:(∗ → (∗ → ∗))⊤] = [⊤λx:∗ λy:∗ x:∗⊤]]
349, 31weqi 76 . . . . . . . . . . 11 [x:∗ = ⊤]:∗
3534id 25 . . . . . . . . . 10 [x:∗ = ⊤]⊧[x:∗ = ⊤]
3623, 31weqi 76 . . . . . . . . . . 11 [y:∗ = ⊤]:∗
3736, 31eqid 83 . . . . . . . . . 10 [y:∗ = ⊤]⊧[⊤ = ⊤]
389, 31, 31, 35, 37ovl 117 . . . . . . . . 9 ⊤⊧[[⊤λx:∗ λy:∗ x:∗⊤] = ⊤]
3918, 38a1i 28 . . . . . . . 8 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[⊤λx:∗ λy:∗ x:∗⊤] = ⊤]
4032, 33, 39eqtri 95 . . . . . . 7 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ x:∗]⊧[[⊤f:(∗ → (∗ → ∗))⊤] = ⊤]
4132, 11, 40cl 116 . . . . . 6 ⊤⊧[(λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ x:∗) = ⊤]
424, 41a1i 28 . . . . 5 [A B]⊧[(λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ x:∗) = ⊤]
4312, 17, 30, 423eqtr3i 97 . . . 4 [A B]⊧[A = ⊤]
445, 43mpbir 87 . . 3 [A B]⊧A
4523wl 66 . . . . . . 7 λy:∗ y:∗:(∗ → ∗)
4645wl 66 . . . . . 6 λx:∗ λy:∗ y:∗:(∗ → (∗ → ∗))
478, 46wc 50 . . . . 5 (λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗):∗
488, 46, 16ceq1 89 . . . . 5 [A B]⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗) = (λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ y:∗)]
496, 46weqi 76 . . . . . . . . . 10 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]:∗
5049id 25 . . . . . . . . 9 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]
516, 2, 3, 50oveq 102 . . . . . . . 8 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[[Af:(∗ → (∗ → ∗))B] = [Aλx:∗ λy:∗ y:∗B]]
527, 46, 51cl 116 . . . . . . 7 ⊤⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗) = [Aλx:∗ λy:∗ y:∗B]]
5321, 23eqid 83 . . . . . . . . 9 [x:∗ = A]⊧[y:∗ = y:∗]
5424id 25 . . . . . . . . 9 [y:∗ = B]⊧[y:∗ = B]
5523, 2, 3, 53, 54ovl 117 . . . . . . . 8 ⊤⊧[[Aλx:∗ λy:∗ y:∗B] = B]
5631, 55a1i 28 . . . . . . 7 ⊤⊧[[Aλx:∗ λy:∗ y:∗B] = B]
5747, 52, 56eqtri 95 . . . . . 6 ⊤⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗) = B]
584, 57a1i 28 . . . . 5 [A B]⊧[(λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B]λx:∗ λy:∗ y:∗) = B]
596, 31, 31, 50oveq 102 . . . . . . . 8 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[[⊤f:(∗ → (∗ → ∗))⊤] = [⊤λx:∗ λy:∗ y:∗⊤]]
6034, 23eqid 83 . . . . . . . . . 10 [x:∗ = ⊤]⊧[y:∗ = y:∗]
6136id 25 . . . . . . . . . 10 [y:∗ = ⊤]⊧[y:∗ = ⊤]
6223, 31, 31, 60, 61ovl 117 . . . . . . . . 9 ⊤⊧[[⊤λx:∗ λy:∗ y:∗⊤] = ⊤]
6349, 62a1i 28 . . . . . . . 8 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[[⊤λx:∗ λy:∗ y:∗⊤] = ⊤]
6432, 59, 63eqtri 95 . . . . . . 7 [f:(∗ → (∗ → ∗)) = λx:∗ λy:∗ y:∗]⊧[[⊤f:(∗ → (∗ → ∗))⊤] = ⊤]
6532, 46, 64cl 116 . . . . . 6 ⊤⊧[(λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ y:∗) = ⊤]
664, 65a1i 28 . . . . 5 [A B]⊧[(λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]λx:∗ λy:∗ y:∗) = ⊤]
6747, 48, 58, 663eqtr3i 97 . . . 4 [A B]⊧[B = ⊤]
685, 67mpbir 87 . . 3 [A B]⊧B
6944, 68jca 18 . 2 [A B]⊧(A, B)
702, 3simpl 22 . . . . . . 7 (A, B)⊧A
7170eqtru 86 . . . . . 6 (A, B)⊧[⊤ = A]
722, 3simpr 23 . . . . . . 7 (A, B)⊧B
7372eqtru 86 . . . . . 6 (A, B)⊧[⊤ = B]
746, 31, 31, 71, 73oveq12 100 . . . . 5 (A, B)⊧[[⊤f:(∗ → (∗ → ∗))⊤] = [Af:(∗ → (∗ → ∗))B]]
7532, 74eqcomi 79 . . . 4 (A, B)⊧[[Af:(∗ → (∗ → ∗))B] = [⊤f:(∗ → (∗ → ∗))⊤]]
767, 75leq 91 . . 3 (A, B)⊧[λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]
7770ax-cb1 29 . . . 4 (A, B):∗
7877, 14a1i 28 . . 3 (A, B)⊧[[A B] = [λf:(∗ → (∗ → ∗)) [Af:(∗ → (∗ → ∗))B] = λf:(∗ → (∗ → ∗)) [⊤f:(∗ → (∗ → ∗))⊤]]]
7976, 78mpbir 87 . 2 (A, B)⊧[A B]
8069, 79dedi 85 1 ⊤⊧[[A B] = (A, B)]
 Colors of variables: type var term 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
 Copyright terms: Public domain W3C validator