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 39958
Description: Set 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 9164; 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 1915 . . . . . . . . . . 11 𝑥Tr 𝑦
2 nfa1 2153 . . . . . . . . . . 11 𝑥𝑥(𝑥𝐴𝑥𝐴)
31, 2nfan 1900 . . . . . . . . . 10 𝑥(Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴))
4 eldifn 4058 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑦𝐴) → ¬ 𝑥𝐴)
54adantl 485 . . . . . . . . . . . . 13 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ 𝑥𝐴)
6 trss 5148 . . . . . . . . . . . . . . . . . 18 (Tr 𝑦 → (𝑥𝑦𝑥𝑦))
7 eldifi 4057 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦𝐴) → 𝑥𝑦)
86, 7impel 509 . . . . . . . . . . . . . . . . 17 ((Tr 𝑦𝑥 ∈ (𝑦𝐴)) → 𝑥𝑦)
9 df-ss 3901 . . . . . . . . . . . . . . . . 17 (𝑥𝑦 ↔ (𝑥𝑦) = 𝑥)
108, 9sylib 221 . . . . . . . . . . . . . . . 16 ((Tr 𝑦𝑥 ∈ (𝑦𝐴)) → (𝑥𝑦) = 𝑥)
1110adantlr 714 . . . . . . . . . . . . . . 15 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → (𝑥𝑦) = 𝑥)
1211sseq1d 3949 . . . . . . . . . . . . . 14 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ((𝑥𝑦) ⊆ 𝐴𝑥𝐴))
13 sp 2181 . . . . . . . . . . . . . . 15 (∀𝑥(𝑥𝐴𝑥𝐴) → (𝑥𝐴𝑥𝐴))
1413ad2antlr 726 . . . . . . . . . . . . . 14 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → (𝑥𝐴𝑥𝐴))
1512, 14sylbid 243 . . . . . . . . . . . . 13 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ((𝑥𝑦) ⊆ 𝐴𝑥𝐴))
165, 15mtod 201 . . . . . . . . . . . 12 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ (𝑥𝑦) ⊆ 𝐴)
17 inssdif0 4286 . . . . . . . . . . . 12 ((𝑥𝑦) ⊆ 𝐴 ↔ (𝑥 ∩ (𝑦𝐴)) = ∅)
1816, 17sylnib 331 . . . . . . . . . . 11 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ (𝑥 ∩ (𝑦𝐴)) = ∅)
1918ex 416 . . . . . . . . . 10 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → (𝑥 ∈ (𝑦𝐴) → ¬ (𝑥 ∩ (𝑦𝐴)) = ∅))
203, 19ralrimi 3183 . . . . . . . . 9 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → ∀𝑥 ∈ (𝑦𝐴) ¬ (𝑥 ∩ (𝑦𝐴)) = ∅)
21 ralnex 3202 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝐴) ¬ (𝑥 ∩ (𝑦𝐴)) = ∅ ↔ ¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2220, 21sylib 221 . . . . . . . 8 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → ¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
23 vex 3447 . . . . . . . . . . 11 𝑦 ∈ V
2423difexi 5199 . . . . . . . . . 10 (𝑦𝐴) ∈ V
25 zfreg 9047 . . . . . . . . . 10 (((𝑦𝐴) ∈ V ∧ (𝑦𝐴) ≠ ∅) → ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2624, 25mpan 689 . . . . . . . . 9 ((𝑦𝐴) ≠ ∅ → ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2726necon1bi 3018 . . . . . . . 8 (¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅ → (𝑦𝐴) = ∅)
2822, 27syl 17 . . . . . . 7 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → (𝑦𝐴) = ∅)
29 ssdif0 4280 . . . . . . 7 (𝑦𝐴 ↔ (𝑦𝐴) = ∅)
3028, 29sylibr 237 . . . . . 6 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝑦𝐴)
3130adantlr 714 . . . . 5 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝑦𝐴)
32 simplr 768 . . . . 5 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝐵𝑦)
3331, 32sseldd 3919 . . . 4 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝐵𝐴)
3433ex 416 . . 3 ((Tr 𝑦𝐵𝑦) → (∀𝑥(𝑥𝐴𝑥𝐴) → 𝐵𝐴))
3534exlimiv 1931 . 2 (∃𝑦(Tr 𝑦𝐵𝑦) → (∀𝑥(𝑥𝐴𝑥𝐴) → 𝐵𝐴))
3635com12 32 1 (∀𝑥(𝑥𝐴𝑥𝐴) → (∃𝑦(Tr 𝑦𝐵𝑦) → 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wal 1536   = wceq 1538  wex 1781  wcel 2112  wne 2990  wral 3109  wrex 3110  Vcvv 3444  cdif 3881  cin 3883  wss 3884  c0 4246  Tr wtr 5139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-reg 9044
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-dif 3887  df-in 3891  df-ss 3901  df-nul 4247  df-uni 4804  df-tr 5140
This theorem is referenced by:  setindtrs  39959
  Copyright terms: Public domain W3C validator