MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elwina Structured version   Visualization version   GIF version

Theorem elwina 9364
Description: Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.)
Assertion
Ref Expression
elwina (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 𝑥𝑦))
Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem elwina
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 elex 3184 . 2 (𝐴 ∈ Inaccw𝐴 ∈ V)
2 fvex 6098 . . . 4 (cf‘𝐴) ∈ V
3 eleq1 2675 . . . 4 ((cf‘𝐴) = 𝐴 → ((cf‘𝐴) ∈ V ↔ 𝐴 ∈ V))
42, 3mpbii 221 . . 3 ((cf‘𝐴) = 𝐴𝐴 ∈ V)
543ad2ant2 1075 . 2 ((𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 𝑥𝑦) → 𝐴 ∈ V)
6 neeq1 2843 . . . 4 (𝑧 = 𝐴 → (𝑧 ≠ ∅ ↔ 𝐴 ≠ ∅))
7 fveq2 6088 . . . . 5 (𝑧 = 𝐴 → (cf‘𝑧) = (cf‘𝐴))
8 eqeq12 2622 . . . . 5 (((cf‘𝑧) = (cf‘𝐴) ∧ 𝑧 = 𝐴) → ((cf‘𝑧) = 𝑧 ↔ (cf‘𝐴) = 𝐴))
97, 8mpancom 699 . . . 4 (𝑧 = 𝐴 → ((cf‘𝑧) = 𝑧 ↔ (cf‘𝐴) = 𝐴))
10 rexeq 3115 . . . . 5 (𝑧 = 𝐴 → (∃𝑦𝑧 𝑥𝑦 ↔ ∃𝑦𝐴 𝑥𝑦))
1110raleqbi1dv 3122 . . . 4 (𝑧 = 𝐴 → (∀𝑥𝑧𝑦𝑧 𝑥𝑦 ↔ ∀𝑥𝐴𝑦𝐴 𝑥𝑦))
126, 9, 113anbi123d 1390 . . 3 (𝑧 = 𝐴 → ((𝑧 ≠ ∅ ∧ (cf‘𝑧) = 𝑧 ∧ ∀𝑥𝑧𝑦𝑧 𝑥𝑦) ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 𝑥𝑦)))
13 df-wina 9362 . . 3 Inaccw = {𝑧 ∣ (𝑧 ≠ ∅ ∧ (cf‘𝑧) = 𝑧 ∧ ∀𝑥𝑧𝑦𝑧 𝑥𝑦)}
1412, 13elab2g 3321 . 2 (𝐴 ∈ V → (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 𝑥𝑦)))
151, 5, 14pm5.21nii 366 1 (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 𝑥𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 194  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  Vcvv 3172  c0 3873   class class class wbr 4577  cfv 5790  csdm 7817  cfccf 8623  Inaccwcwina 9360
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-nul 4712
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-wina 9362
This theorem is referenced by:  winaon  9366  inawina  9368  winacard  9370  winainf  9372  winalim2  9374  winafp  9375  gchina  9377
  Copyright terms: Public domain W3C validator