Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wzel Structured version   Visualization version   GIF version

Theorem wzel 32090
Description: The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.)
Assertion
Ref Expression
wzel ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴)

Proof of Theorem wzel
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 weso 5302 . . 3 (𝑅 We 𝐴𝑅 Or 𝐴)
213ad2ant1 1156 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → 𝑅 Or 𝐴)
3 simp1 1159 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → 𝑅 We 𝐴)
4 simp2 1160 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → 𝑅 Se 𝐴)
5 ssidd 3821 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → 𝐴𝐴)
6 simp3 1161 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → 𝐴 ≠ ∅)
7 tz6.26 5924 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝐴𝐴𝐴 ≠ ∅)) → ∃𝑥𝐴 Pred(𝑅, 𝐴, 𝑥) = ∅)
83, 4, 5, 6, 7syl22anc 858 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → ∃𝑥𝐴 Pred(𝑅, 𝐴, 𝑥) = ∅)
9 vex 3394 . . . . . . . . . . . 12 𝑥 ∈ V
10 vex 3394 . . . . . . . . . . . . 13 𝑦 ∈ V
1110elpred 5906 . . . . . . . . . . . 12 (𝑥 ∈ V → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) ↔ (𝑦𝐴𝑦𝑅𝑥)))
129, 11ax-mp 5 . . . . . . . . . . 11 (𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) ↔ (𝑦𝐴𝑦𝑅𝑥))
1312notbii 311 . . . . . . . . . 10 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) ↔ ¬ (𝑦𝐴𝑦𝑅𝑥))
14 imnan 388 . . . . . . . . . 10 ((𝑦𝐴 → ¬ 𝑦𝑅𝑥) ↔ ¬ (𝑦𝐴𝑦𝑅𝑥))
1513, 14bitr4i 269 . . . . . . . . 9 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) ↔ (𝑦𝐴 → ¬ 𝑦𝑅𝑥))
16 pm2.27 42 . . . . . . . . . . 11 (𝑦𝐴 → ((𝑦𝐴 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥))
1716ad2antll 711 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) ∧ (𝑥𝐴𝑦𝐴)) → ((𝑦𝐴 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥))
18 breq1 4847 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → (𝑧𝑅𝑦𝑥𝑅𝑦))
1918rspcev 3502 . . . . . . . . . . . 12 ((𝑥𝐴𝑥𝑅𝑦) → ∃𝑧𝐴 𝑧𝑅𝑦)
2019ex 399 . . . . . . . . . . 11 (𝑥𝐴 → (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦))
2120ad2antrl 710 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) ∧ (𝑥𝐴𝑦𝐴)) → (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦))
2217, 21jctird 518 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) ∧ (𝑥𝐴𝑦𝐴)) → ((𝑦𝐴 → ¬ 𝑦𝑅𝑥) → (¬ 𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦))))
2315, 22syl5bi 233 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) ∧ (𝑥𝐴𝑦𝐴)) → (¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) → (¬ 𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦))))
2423expr 446 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) ∧ 𝑥𝐴) → (𝑦𝐴 → (¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) → (¬ 𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦)))))
2524com23 86 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) ∧ 𝑥𝐴) → (¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) → (𝑦𝐴 → (¬ 𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦)))))
2625alimdv 2007 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) ∧ 𝑥𝐴) → (∀𝑦 ¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) → ∀𝑦(𝑦𝐴 → (¬ 𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦)))))
27 eq0 4130 . . . . 5 (Pred(𝑅, 𝐴, 𝑥) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥))
28 r19.26 3252 . . . . . 6 (∀𝑦𝐴𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦)) ↔ (∀𝑦𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦𝐴 (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦)))
29 df-ral 3101 . . . . . 6 (∀𝑦𝐴𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦)) ↔ ∀𝑦(𝑦𝐴 → (¬ 𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦))))
3028, 29bitr3i 268 . . . . 5 ((∀𝑦𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦𝐴 (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦)) ↔ ∀𝑦(𝑦𝐴 → (¬ 𝑦𝑅𝑥 ∧ (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦))))
3126, 27, 303imtr4g 287 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) ∧ 𝑥𝐴) → (Pred(𝑅, 𝐴, 𝑥) = ∅ → (∀𝑦𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦𝐴 (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦))))
3231reximdva 3204 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → (∃𝑥𝐴 Pred(𝑅, 𝐴, 𝑥) = ∅ → ∃𝑥𝐴 (∀𝑦𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦𝐴 (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦))))
338, 32mpd 15 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → ∃𝑥𝐴 (∀𝑦𝐴 ¬ 𝑦𝑅𝑥 ∧ ∀𝑦𝐴 (𝑥𝑅𝑦 → ∃𝑧𝐴 𝑧𝑅𝑦)))
342, 33infcl 8633 1 ((𝑅 We 𝐴𝑅 Se 𝐴𝐴 ≠ ∅) → inf(𝐴, 𝐴, 𝑅) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100  wal 1635   = wceq 1637  wcel 2156  wne 2978  wral 3096  wrex 3097  Vcvv 3391  wss 3769  c0 4116   class class class wbr 4844   Or wor 5231   Se wse 5268   We wwe 5269  Predcpred 5892  infcinf 8586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-cnv 5319  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-iota 6064  df-riota 6835  df-sup 8587  df-inf 8588
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator