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 38564
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 8909; 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 1957 . . . . . . . . . . 11 𝑥Tr 𝑦
2 nfa1 2145 . . . . . . . . . . 11 𝑥𝑥(𝑥𝐴𝑥𝐴)
31, 2nfan 1946 . . . . . . . . . 10 𝑥(Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴))
4 eldifn 3956 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑦𝐴) → ¬ 𝑥𝐴)
54adantl 475 . . . . . . . . . . . . 13 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ 𝑥𝐴)
6 trss 4998 . . . . . . . . . . . . . . . . . 18 (Tr 𝑦 → (𝑥𝑦𝑥𝑦))
7 eldifi 3955 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦𝐴) → 𝑥𝑦)
86, 7impel 501 . . . . . . . . . . . . . . . . 17 ((Tr 𝑦𝑥 ∈ (𝑦𝐴)) → 𝑥𝑦)
9 df-ss 3806 . . . . . . . . . . . . . . . . 17 (𝑥𝑦 ↔ (𝑥𝑦) = 𝑥)
108, 9sylib 210 . . . . . . . . . . . . . . . 16 ((Tr 𝑦𝑥 ∈ (𝑦𝐴)) → (𝑥𝑦) = 𝑥)
1110adantlr 705 . . . . . . . . . . . . . . 15 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → (𝑥𝑦) = 𝑥)
1211sseq1d 3851 . . . . . . . . . . . . . 14 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ((𝑥𝑦) ⊆ 𝐴𝑥𝐴))
13 sp 2167 . . . . . . . . . . . . . . 15 (∀𝑥(𝑥𝐴𝑥𝐴) → (𝑥𝐴𝑥𝐴))
1413ad2antlr 717 . . . . . . . . . . . . . 14 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → (𝑥𝐴𝑥𝐴))
1512, 14sylbid 232 . . . . . . . . . . . . 13 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ((𝑥𝑦) ⊆ 𝐴𝑥𝐴))
165, 15mtod 190 . . . . . . . . . . . 12 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ (𝑥𝑦) ⊆ 𝐴)
17 inssdif0 4178 . . . . . . . . . . . 12 ((𝑥𝑦) ⊆ 𝐴 ↔ (𝑥 ∩ (𝑦𝐴)) = ∅)
1816, 17sylnib 320 . . . . . . . . . . 11 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ (𝑥 ∩ (𝑦𝐴)) = ∅)
1918ex 403 . . . . . . . . . 10 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → (𝑥 ∈ (𝑦𝐴) → ¬ (𝑥 ∩ (𝑦𝐴)) = ∅))
203, 19ralrimi 3139 . . . . . . . . 9 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → ∀𝑥 ∈ (𝑦𝐴) ¬ (𝑥 ∩ (𝑦𝐴)) = ∅)
21 ralnex 3174 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝐴) ¬ (𝑥 ∩ (𝑦𝐴)) = ∅ ↔ ¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2220, 21sylib 210 . . . . . . . 8 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → ¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
23 vex 3401 . . . . . . . . . . 11 𝑦 ∈ V
2423difexi 5048 . . . . . . . . . 10 (𝑦𝐴) ∈ V
25 zfreg 8791 . . . . . . . . . 10 (((𝑦𝐴) ∈ V ∧ (𝑦𝐴) ≠ ∅) → ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2624, 25mpan 680 . . . . . . . . 9 ((𝑦𝐴) ≠ ∅ → ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2726necon1bi 2997 . . . . . . . 8 (¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅ → (𝑦𝐴) = ∅)
2822, 27syl 17 . . . . . . 7 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → (𝑦𝐴) = ∅)
29 ssdif0 4172 . . . . . . 7 (𝑦𝐴 ↔ (𝑦𝐴) = ∅)
3028, 29sylibr 226 . . . . . 6 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝑦𝐴)
3130adantlr 705 . . . . 5 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝑦𝐴)
32 simplr 759 . . . . 5 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝐵𝑦)
3331, 32sseldd 3822 . . . 4 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝐵𝐴)
3433ex 403 . . 3 ((Tr 𝑦𝐵𝑦) → (∀𝑥(𝑥𝐴𝑥𝐴) → 𝐵𝐴))
3534exlimiv 1973 . 2 (∃𝑦(Tr 𝑦𝐵𝑦) → (∀𝑥(𝑥𝐴𝑥𝐴) → 𝐵𝐴))
3635com12 32 1 (∀𝑥(𝑥𝐴𝑥𝐴) → (∃𝑦(Tr 𝑦𝐵𝑦) → 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386  wal 1599   = wceq 1601  wex 1823  wcel 2107  wne 2969  wral 3090  wrex 3091  Vcvv 3398  cdif 3789  cin 3791  wss 3792  c0 4141  Tr wtr 4989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754  ax-sep 5019  ax-reg 8788
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-v 3400  df-dif 3795  df-in 3799  df-ss 3806  df-nul 4142  df-uni 4674  df-tr 4990
This theorem is referenced by:  setindtrs  38565
  Copyright terms: Public domain W3C validator