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 38117
 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 8774; 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 1995 . . . . . . . . . . 11 𝑥Tr 𝑦
2 nfa1 2184 . . . . . . . . . . 11 𝑥𝑥(𝑥𝐴𝑥𝐴)
31, 2nfan 1980 . . . . . . . . . 10 𝑥(Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴))
4 eldifn 3884 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝑦𝐴) → ¬ 𝑥𝐴)
54adantl 467 . . . . . . . . . . . . 13 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ 𝑥𝐴)
6 trss 4895 . . . . . . . . . . . . . . . . . 18 (Tr 𝑦 → (𝑥𝑦𝑥𝑦))
7 eldifi 3883 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝑦𝐴) → 𝑥𝑦)
86, 7impel 495 . . . . . . . . . . . . . . . . 17 ((Tr 𝑦𝑥 ∈ (𝑦𝐴)) → 𝑥𝑦)
9 df-ss 3737 . . . . . . . . . . . . . . . . 17 (𝑥𝑦 ↔ (𝑥𝑦) = 𝑥)
108, 9sylib 208 . . . . . . . . . . . . . . . 16 ((Tr 𝑦𝑥 ∈ (𝑦𝐴)) → (𝑥𝑦) = 𝑥)
1110adantlr 694 . . . . . . . . . . . . . . 15 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → (𝑥𝑦) = 𝑥)
1211sseq1d 3781 . . . . . . . . . . . . . 14 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ((𝑥𝑦) ⊆ 𝐴𝑥𝐴))
13 sp 2207 . . . . . . . . . . . . . . 15 (∀𝑥(𝑥𝐴𝑥𝐴) → (𝑥𝐴𝑥𝐴))
1413ad2antlr 706 . . . . . . . . . . . . . 14 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → (𝑥𝐴𝑥𝐴))
1512, 14sylbid 230 . . . . . . . . . . . . 13 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ((𝑥𝑦) ⊆ 𝐴𝑥𝐴))
165, 15mtod 189 . . . . . . . . . . . 12 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ (𝑥𝑦) ⊆ 𝐴)
17 inssdif0 4094 . . . . . . . . . . . 12 ((𝑥𝑦) ⊆ 𝐴 ↔ (𝑥 ∩ (𝑦𝐴)) = ∅)
1816, 17sylnib 317 . . . . . . . . . . 11 (((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) ∧ 𝑥 ∈ (𝑦𝐴)) → ¬ (𝑥 ∩ (𝑦𝐴)) = ∅)
1918ex 397 . . . . . . . . . 10 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → (𝑥 ∈ (𝑦𝐴) → ¬ (𝑥 ∩ (𝑦𝐴)) = ∅))
203, 19ralrimi 3106 . . . . . . . . 9 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → ∀𝑥 ∈ (𝑦𝐴) ¬ (𝑥 ∩ (𝑦𝐴)) = ∅)
21 ralnex 3141 . . . . . . . . 9 (∀𝑥 ∈ (𝑦𝐴) ¬ (𝑥 ∩ (𝑦𝐴)) = ∅ ↔ ¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2220, 21sylib 208 . . . . . . . 8 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → ¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
23 vex 3354 . . . . . . . . . . 11 𝑦 ∈ V
2423difexi 4943 . . . . . . . . . 10 (𝑦𝐴) ∈ V
25 zfreg 8656 . . . . . . . . . 10 (((𝑦𝐴) ∈ V ∧ (𝑦𝐴) ≠ ∅) → ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2624, 25mpan 670 . . . . . . . . 9 ((𝑦𝐴) ≠ ∅ → ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅)
2726necon1bi 2971 . . . . . . . 8 (¬ ∃𝑥 ∈ (𝑦𝐴)(𝑥 ∩ (𝑦𝐴)) = ∅ → (𝑦𝐴) = ∅)
2822, 27syl 17 . . . . . . 7 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → (𝑦𝐴) = ∅)
29 ssdif0 4089 . . . . . . 7 (𝑦𝐴 ↔ (𝑦𝐴) = ∅)
3028, 29sylibr 224 . . . . . 6 ((Tr 𝑦 ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝑦𝐴)
3130adantlr 694 . . . . 5 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝑦𝐴)
32 simplr 752 . . . . 5 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝐵𝑦)
3331, 32sseldd 3753 . . . 4 (((Tr 𝑦𝐵𝑦) ∧ ∀𝑥(𝑥𝐴𝑥𝐴)) → 𝐵𝐴)
3433ex 397 . . 3 ((Tr 𝑦𝐵𝑦) → (∀𝑥(𝑥𝐴𝑥𝐴) → 𝐵𝐴))
3534exlimiv 2010 . 2 (∃𝑦(Tr 𝑦𝐵𝑦) → (∀𝑥(𝑥𝐴𝑥𝐴) → 𝐵𝐴))
3635com12 32 1 (∀𝑥(𝑥𝐴𝑥𝐴) → (∃𝑦(Tr 𝑦𝐵𝑦) → 𝐵𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 382  ∀wal 1629   = wceq 1631  ∃wex 1852   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  ∃wrex 3062  Vcvv 3351   ∖ cdif 3720   ∩ cin 3722   ⊆ wss 3723  ∅c0 4063  Tr wtr 4886 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-reg 8653 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064  df-uni 4575  df-tr 4887 This theorem is referenced by:  setindtrs  38118
 Copyright terms: Public domain W3C validator