Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  setindtr Structured version   Visualization version   GIF version

Theorem setindtr 37410
Description: Epsilon induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind 8595; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.)
Assertion
Ref Expression
setindtr (∀𝑥(𝑥𝐴𝑥𝐴) → (∃𝑦(Tr 𝑦𝐵𝑦) → 𝐵𝐴))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem setindtr
StepHypRef Expression
1 nfv 1841 . . . . . . . . . . 11 𝑥Tr 𝑦
2 nfa1 2026 . . . . . . . . . . 11 𝑥𝑥(𝑥𝐴𝑥𝐴)
31, 2nfan 1826 . . . . . . . . . 10 𝑥(Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴))
4 eldifn 3725 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑦𝐴) → ¬ 𝑥𝐴)
54adantl 482 . . . . . . . . . . . . 13 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ 𝑥𝐴)
6 trss 4752 . . . . . . . . . . . . . . . . . 18 (Tr 𝑦 → (𝑥𝑦𝑥𝑦))
7 eldifi 3724 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦𝐴) → 𝑥𝑦)
86, 7impel 485 . . . . . . . . . . . . . . . . 17 ((Tr 𝑦𝑥 ∈ (𝑦𝐴)) → 𝑥𝑦)
9 df-ss 3581 . . . . . . . . . . . . . . . . 17 (𝑥𝑦 ↔ (𝑥𝑦) = 𝑥)
108, 9sylib 208 . . . . . . . . . . . . . . . 16 ((Tr 𝑦𝑥 ∈ (𝑦𝐴)) → (𝑥𝑦) = 𝑥)
1110adantlr 750 . . . . . . . . . . . . . . 15 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → (𝑥𝑦) = 𝑥)
1211sseq1d 3624 . . . . . . . . . . . . . 14 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ((𝑥𝑦) ⊆ 𝐴𝑥𝐴))
13 sp 2051 . . . . . . . . . . . . . . 15 (∀𝑥(𝑥𝐴𝑥𝐴) → (𝑥𝐴𝑥𝐴))
1413ad2antlr 762 . . . . . . . . . . . . . 14 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → (𝑥𝐴𝑥𝐴))
1512, 14sylbid 230 . . . . . . . . . . . . 13 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ((𝑥𝑦) ⊆ 𝐴𝑥𝐴))
165, 15mtod 189 . . . . . . . . . . . 12 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ (𝑥𝑦) ⊆ 𝐴)
17 inssdif0 3938 . . . . . . . . . . . 12 ((𝑥𝑦) ⊆ 𝐴 ↔ (𝑥 ∩ (𝑦𝐴)) = ∅)
1816, 17sylnib 318 . . . . . . . . . . 11 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ (𝑥 ∩ (𝑦𝐴)) = ∅)
1918ex 450 . . . . . . . . . 10 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → (𝑥 ∈ (𝑦𝐴) → ¬ (𝑥 ∩ (𝑦𝐴)) = ∅))
203, 19ralrimi 2954 . . . . . . . . 9 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → ∀𝑥 ∈ (𝑦𝐴) ¬ (𝑥 ∩ (𝑦𝐴)) = ∅)
21 ralnex 2989 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝐴) ¬ (𝑥 ∩ (𝑦𝐴)) = ∅ ↔ ¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2220, 21sylib 208 . . . . . . . 8 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → ¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
23 vex 3198 . . . . . . . . . . 11 𝑦 ∈ V
2423difexi 4800 . . . . . . . . . 10 (𝑦𝐴) ∈ V
25 zfreg 8485 . . . . . . . . . 10 (((𝑦𝐴) ∈ V ∧ (𝑦𝐴) ≠ ∅) → ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2624, 25mpan 705 . . . . . . . . 9 ((𝑦𝐴) ≠ ∅ → ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2726necon1bi 2819 . . . . . . . 8 (¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅ → (𝑦𝐴) = ∅)
2822, 27syl 17 . . . . . . 7 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → (𝑦𝐴) = ∅)
29 ssdif0 3933 . . . . . . 7 (𝑦𝐴 ↔ (𝑦𝐴) = ∅)
3028, 29sylibr 224 . . . . . 6 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝑦𝐴)
3130adantlr 750 . . . . 5 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝑦𝐴)
32 simplr 791 . . . . 5 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝐵𝑦)
3331, 32sseldd 3596 . . . 4 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝐵𝐴)
3433ex 450 . . 3 ((Tr 𝑦𝐵𝑦) → (∀𝑥(𝑥𝐴𝑥𝐴) → 𝐵𝐴))
3534exlimiv 1856 . 2 (∃𝑦(Tr 𝑦𝐵𝑦) → (∀𝑥(𝑥𝐴𝑥𝐴) → 𝐵𝐴))
3635com12 32 1 (∀𝑥(𝑥𝐴𝑥𝐴) → (∃𝑦(Tr 𝑦𝐵𝑦) → 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wal 1479   = wceq 1481  wex 1702  wcel 1988  wne 2791  wral 2909  wrex 2910  Vcvv 3195  cdif 3564  cin 3566  wss 3567  c0 3907  Tr wtr 4743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-reg 8482
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-v 3197  df-dif 3570  df-in 3574  df-ss 3581  df-nul 3908  df-uni 4428  df-tr 4744
This theorem is referenced by:  setindtrs  37411
  Copyright terms: Public domain W3C validator