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 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