MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tz9.12lem1 Structured version   Visualization version   GIF version

Theorem tz9.12lem1 9190
Description: Lemma for tz9.12 9193. (Contributed by NM, 22-Sep-2003.) (Revised by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
tz9.12lem.1 𝐴 ∈ V
tz9.12lem.2 𝐹 = (𝑧 ∈ V ↦ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)})
Assertion
Ref Expression
tz9.12lem1 (𝐹𝐴) ⊆ On
Distinct variable group:   𝑧,𝑣,𝐴
Allowed substitution hints:   𝐹(𝑧,𝑣)

Proof of Theorem tz9.12lem1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 imassrn 5912 . 2 (𝐹𝐴) ⊆ ran 𝐹
2 tz9.12lem.2 . . . 4 𝐹 = (𝑧 ∈ V ↦ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)})
32rnmpt 5799 . . 3 ran 𝐹 = {𝑥 ∣ ∃𝑧 ∈ V 𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)}}
4 id 22 . . . . . 6 (𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} → 𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)})
5 ssrab2 4031 . . . . . . 7 {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ⊆ On
6 eqvisset 3487 . . . . . . . 8 (𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} → {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ∈ V)
7 intex 5212 . . . . . . . 8 ({𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ≠ ∅ ↔ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ∈ V)
86, 7sylibr 236 . . . . . . 7 (𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} → {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ≠ ∅)
9 oninton 7489 . . . . . . 7 (({𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ⊆ On ∧ {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ≠ ∅) → {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ∈ On)
105, 8, 9sylancr 589 . . . . . 6 (𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} → {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} ∈ On)
114, 10eqeltrd 2911 . . . . 5 (𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} → 𝑥 ∈ On)
1211rexlimivw 3267 . . . 4 (∃𝑧 ∈ V 𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)} → 𝑥 ∈ On)
1312abssi 4021 . . 3 {𝑥 ∣ ∃𝑧 ∈ V 𝑥 = {𝑣 ∈ On ∣ 𝑧 ∈ (𝑅1𝑣)}} ⊆ On
143, 13eqsstri 3976 . 2 ran 𝐹 ⊆ On
151, 14sstri 3951 1 (𝐹𝐴) ⊆ On
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2114  {cab 2798  wne 3006  wrex 3126  {crab 3129  Vcvv 3470  wss 3909  c0 4265   cint 4848  cmpt 5118  ran crn 5528  cima 5530  Oncon0 6163  cfv 6327  𝑅1cr1 9165
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5175  ax-nul 5182  ax-pr 5302  ax-un 7435
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3472  df-sbc 3749  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4811  df-int 4849  df-br 5039  df-opab 5101  df-mpt 5119  df-tr 5145  df-eprel 5437  df-po 5446  df-so 5447  df-fr 5486  df-we 5488  df-xp 5533  df-cnv 5535  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-ord 6166  df-on 6167
This theorem is referenced by:  tz9.12lem2  9191  tz9.12lem3  9192
  Copyright terms: Public domain W3C validator