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

Theorem axun 209
Description: Axiom of Union. An axiom of Zermelo-Fraenkel set theory.
Hypothesis
Ref Expression
axun.1 A:((α → ∗) → ∗)
Assertion
Ref Expression
axun ⊤⊧(λy:(α → ∗) (λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)]))
Distinct variable groups:   x,y   y,z   y,A   α,y,z

Proof of Theorem axun
Dummy variable p is distinct from all other variables.
StepHypRef Expression
1 wtru 40 . . . . . 6 ⊤:∗
2 wex 129 . . . . . . 7 :(((α → ∗) → ∗) → ∗)
3 wan 126 . . . . . . . . 9 :(∗ → (∗ → ∗))
4 wv 58 . . . . . . . . . 10 x:(α → ∗):(α → ∗)
5 wv 58 . . . . . . . . . 10 z:α:α
64, 5wc 45 . . . . . . . . 9 (x:(α → ∗)z:α):∗
7 axun.1 . . . . . . . . . 10 A:((α → ∗) → ∗)
87, 4wc 45 . . . . . . . . 9 (Ax:(α → ∗)):∗
93, 6, 8wov 64 . . . . . . . 8 [(x:(α → ∗)z:α) (Ax:(α → ∗))]:∗
109wl 59 . . . . . . 7 λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]:((α → ∗) → ∗)
112, 10wc 45 . . . . . 6 (λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]):∗
121, 11wct 44 . . . . 5 (⊤, (λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))])):∗
1312trud 27 . . . 4 (⊤, (λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]))⊧⊤
1413ex 148 . . 3 ⊤⊧[(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ ⊤]
1514alrimiv 141 . 2 ⊤⊧(λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ ⊤])
16 wal 124 . . . 4 :((α → ∗) → ∗)
17 wim 127 . . . . . 6 ⇒ :(∗ → (∗ → ∗))
18 wv 58 . . . . . . 7 y:(α → ∗):(α → ∗)
1918, 5wc 45 . . . . . 6 (y:(α → ∗)z:α):∗
2017, 11, 19wov 64 . . . . 5 [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)]:∗
2120wl 59 . . . 4 λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)]:(α → ∗)
2216, 21wc 45 . . 3 (λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)]):∗
231wl 59 . . 3 λp:α ⊤:(α → ∗)
2418, 23weqi 68 . . . . . . . . 9 [y:(α → ∗) = λp:α ⊤]:∗
2524id 25 . . . . . . . 8 [y:(α → ∗) = λp:α ⊤]⊧[y:(α → ∗) = λp:α ⊤]
2618, 5, 25ceq1 79 . . . . . . 7 [y:(α → ∗) = λp:α ⊤]⊧[(y:(α → ∗)z:α) = (λp:αz:α)]
271, 5, 24a17i 96 . . . . . . 7 [y:(α → ∗) = λp:α ⊤]⊧[(λp:αz:α) = ⊤]
2819, 26, 27eqtri 85 . . . . . 6 [y:(α → ∗) = λp:α ⊤]⊧[(y:(α → ∗)z:α) = ⊤]
2917, 11, 19, 28oveq2 91 . . . . 5 [y:(α → ∗) = λp:α ⊤]⊧[[(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)] = [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ ⊤]]
3020, 29leq 81 . . . 4 [y:(α → ∗) = λp:α ⊤]⊧[λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)] = λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ ⊤]]
3116, 21, 30ceq2 80 . . 3 [y:(α → ∗) = λp:α ⊤]⊧[(λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)]) = (λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ ⊤])]
3222, 23, 31cla4ev 159 . 2 (λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ ⊤])⊧(λy:(α → ∗) (λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)]))
3315, 32syl 16 1 ⊤⊧(λy:(α → ∗) (λz:α [(λx:(α → ∗) [(x:(α → ∗)z:α) (Ax:(α → ∗))]) ⇒ (y:(α → ∗)z:α)]))
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 109  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
This theorem depends on definitions:  df-ov 65  df-al 116  df-an 118  df-im 119  df-ex 121
  Copyright terms: Public domain W3C validator