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

Theorem wdom2d 8430
Description: Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep 4736). (Contributed by Stefan O'Rear, 13-Feb-2015.)
Hypotheses
Ref Expression
wdom2d.a (𝜑𝐴𝑉)
wdom2d.b (𝜑𝐵𝑊)
wdom2d.o ((𝜑𝑥𝐴) → ∃𝑦𝐵 𝑥 = 𝑋)
Assertion
Ref Expression
wdom2d (𝜑𝐴* 𝐵)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑋   𝜑,𝑥,𝑦
Allowed substitution hints:   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)   𝑋(𝑦)

Proof of Theorem wdom2d
Dummy variables 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wdom2d.b . . . . . 6 (𝜑𝐵𝑊)
2 rabexg 4777 . . . . . 6 (𝐵𝑊 → {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ∈ V)
31, 2syl 17 . . . . 5 (𝜑 → {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ∈ V)
4 wdom2d.a . . . . 5 (𝜑𝐴𝑉)
5 xpexg 6914 . . . . 5 (({𝑧𝐵𝑧 / 𝑦𝑋𝐴} ∈ V ∧ 𝐴𝑉) → ({𝑧𝐵𝑧 / 𝑦𝑋𝐴} × 𝐴) ∈ V)
63, 4, 5syl2anc 692 . . . 4 (𝜑 → ({𝑧𝐵𝑧 / 𝑦𝑋𝐴} × 𝐴) ∈ V)
7 csbeq1 3522 . . . . . . . . . 10 (𝑧 = 𝑤𝑧 / 𝑦𝑋 = 𝑤 / 𝑦𝑋)
87eleq1d 2688 . . . . . . . . 9 (𝑧 = 𝑤 → (𝑧 / 𝑦𝑋𝐴𝑤 / 𝑦𝑋𝐴))
98elrab 3351 . . . . . . . 8 (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↔ (𝑤𝐵𝑤 / 𝑦𝑋𝐴))
109simprbi 480 . . . . . . 7 (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} → 𝑤 / 𝑦𝑋𝐴)
1110adantl 482 . . . . . 6 ((𝜑𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴}) → 𝑤 / 𝑦𝑋𝐴)
12 eqid 2626 . . . . . 6 (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋) = (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)
1311, 12fmptd 6341 . . . . 5 (𝜑 → (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋):{𝑧𝐵𝑧 / 𝑦𝑋𝐴}⟶𝐴)
14 fssxp 6019 . . . . 5 ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋):{𝑧𝐵𝑧 / 𝑦𝑋𝐴}⟶𝐴 → (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋) ⊆ ({𝑧𝐵𝑧 / 𝑦𝑋𝐴} × 𝐴))
1513, 14syl 17 . . . 4 (𝜑 → (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋) ⊆ ({𝑧𝐵𝑧 / 𝑦𝑋𝐴} × 𝐴))
166, 15ssexd 4770 . . 3 (𝜑 → (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋) ∈ V)
17 wdom2d.o . . . . . . . 8 ((𝜑𝑥𝐴) → ∃𝑦𝐵 𝑥 = 𝑋)
18 eleq1 2692 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝑥𝐴𝑋𝐴))
1918biimpcd 239 . . . . . . . . . . 11 (𝑥𝐴 → (𝑥 = 𝑋𝑋𝐴))
2019ancrd 576 . . . . . . . . . 10 (𝑥𝐴 → (𝑥 = 𝑋 → (𝑋𝐴𝑥 = 𝑋)))
2120adantl 482 . . . . . . . . 9 ((𝜑𝑥𝐴) → (𝑥 = 𝑋 → (𝑋𝐴𝑥 = 𝑋)))
2221reximdv 3015 . . . . . . . 8 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝑥 = 𝑋 → ∃𝑦𝐵 (𝑋𝐴𝑥 = 𝑋)))
2317, 22mpd 15 . . . . . . 7 ((𝜑𝑥𝐴) → ∃𝑦𝐵 (𝑋𝐴𝑥 = 𝑋))
24 nfv 1845 . . . . . . . 8 𝑣(𝑋𝐴𝑥 = 𝑋)
25 nfcsb1v 3535 . . . . . . . . . 10 𝑦𝑣 / 𝑦𝑋
2625nfel1 2781 . . . . . . . . 9 𝑦𝑣 / 𝑦𝑋𝐴
2725nfeq2 2782 . . . . . . . . 9 𝑦 𝑥 = 𝑣 / 𝑦𝑋
2826, 27nfan 1830 . . . . . . . 8 𝑦(𝑣 / 𝑦𝑋𝐴𝑥 = 𝑣 / 𝑦𝑋)
29 csbeq1a 3528 . . . . . . . . . 10 (𝑦 = 𝑣𝑋 = 𝑣 / 𝑦𝑋)
3029eleq1d 2688 . . . . . . . . 9 (𝑦 = 𝑣 → (𝑋𝐴𝑣 / 𝑦𝑋𝐴))
3129eqeq2d 2636 . . . . . . . . 9 (𝑦 = 𝑣 → (𝑥 = 𝑋𝑥 = 𝑣 / 𝑦𝑋))
3230, 31anbi12d 746 . . . . . . . 8 (𝑦 = 𝑣 → ((𝑋𝐴𝑥 = 𝑋) ↔ (𝑣 / 𝑦𝑋𝐴𝑥 = 𝑣 / 𝑦𝑋)))
3324, 28, 32cbvrex 3161 . . . . . . 7 (∃𝑦𝐵 (𝑋𝐴𝑥 = 𝑋) ↔ ∃𝑣𝐵 (𝑣 / 𝑦𝑋𝐴𝑥 = 𝑣 / 𝑦𝑋))
3423, 33sylib 208 . . . . . 6 ((𝜑𝑥𝐴) → ∃𝑣𝐵 (𝑣 / 𝑦𝑋𝐴𝑥 = 𝑣 / 𝑦𝑋))
35 csbeq1 3522 . . . . . . . . . . . . 13 (𝑧 = 𝑣𝑧 / 𝑦𝑋 = 𝑣 / 𝑦𝑋)
3635eleq1d 2688 . . . . . . . . . . . 12 (𝑧 = 𝑣 → (𝑧 / 𝑦𝑋𝐴𝑣 / 𝑦𝑋𝐴))
3736elrab 3351 . . . . . . . . . . 11 (𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↔ (𝑣𝐵𝑣 / 𝑦𝑋𝐴))
3837simprbi 480 . . . . . . . . . 10 (𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} → 𝑣 / 𝑦𝑋𝐴)
39 csbeq1 3522 . . . . . . . . . . 11 (𝑤 = 𝑣𝑤 / 𝑦𝑋 = 𝑣 / 𝑦𝑋)
4039, 12fvmptg 6238 . . . . . . . . . 10 ((𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ∧ 𝑣 / 𝑦𝑋𝐴) → ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)‘𝑣) = 𝑣 / 𝑦𝑋)
4138, 40mpdan 701 . . . . . . . . 9 (𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} → ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)‘𝑣) = 𝑣 / 𝑦𝑋)
4241eqeq2d 2636 . . . . . . . 8 (𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} → (𝑥 = ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)‘𝑣) ↔ 𝑥 = 𝑣 / 𝑦𝑋))
4342rexbiia 3038 . . . . . . 7 (∃𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴}𝑥 = ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)‘𝑣) ↔ ∃𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴}𝑥 = 𝑣 / 𝑦𝑋)
4436rexrab 3357 . . . . . . 7 (∃𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴}𝑥 = 𝑣 / 𝑦𝑋 ↔ ∃𝑣𝐵 (𝑣 / 𝑦𝑋𝐴𝑥 = 𝑣 / 𝑦𝑋))
4543, 44bitri 264 . . . . . 6 (∃𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴}𝑥 = ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)‘𝑣) ↔ ∃𝑣𝐵 (𝑣 / 𝑦𝑋𝐴𝑥 = 𝑣 / 𝑦𝑋))
4634, 45sylibr 224 . . . . 5 ((𝜑𝑥𝐴) → ∃𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴}𝑥 = ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)‘𝑣))
4746ralrimiva 2965 . . . 4 (𝜑 → ∀𝑥𝐴𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴}𝑥 = ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)‘𝑣))
48 dffo3 6331 . . . 4 ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋):{𝑧𝐵𝑧 / 𝑦𝑋𝐴}–onto𝐴 ↔ ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋):{𝑧𝐵𝑧 / 𝑦𝑋𝐴}⟶𝐴 ∧ ∀𝑥𝐴𝑣 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴}𝑥 = ((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋)‘𝑣)))
4913, 47, 48sylanbrc 697 . . 3 (𝜑 → (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋):{𝑧𝐵𝑧 / 𝑦𝑋𝐴}–onto𝐴)
50 fowdom 8421 . . 3 (((𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋) ∈ V ∧ (𝑤 ∈ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ↦ 𝑤 / 𝑦𝑋):{𝑧𝐵𝑧 / 𝑦𝑋𝐴}–onto𝐴) → 𝐴* {𝑧𝐵𝑧 / 𝑦𝑋𝐴})
5116, 49, 50syl2anc 692 . 2 (𝜑𝐴* {𝑧𝐵𝑧 / 𝑦𝑋𝐴})
52 ssrab2 3671 . . . 4 {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ⊆ 𝐵
53 ssdomg 7946 . . . 4 (𝐵𝑊 → ({𝑧𝐵𝑧 / 𝑦𝑋𝐴} ⊆ 𝐵 → {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ≼ 𝐵))
5452, 53mpi 20 . . 3 (𝐵𝑊 → {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ≼ 𝐵)
55 domwdom 8424 . . 3 ({𝑧𝐵𝑧 / 𝑦𝑋𝐴} ≼ 𝐵 → {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ≼* 𝐵)
561, 54, 553syl 18 . 2 (𝜑 → {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ≼* 𝐵)
57 wdomtr 8425 . 2 ((𝐴* {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ∧ {𝑧𝐵𝑧 / 𝑦𝑋𝐴} ≼* 𝐵) → 𝐴* 𝐵)
5851, 56, 57syl2anc 692 1 (𝜑𝐴* 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1992  wral 2912  wrex 2913  {crab 2916  Vcvv 3191  csb 3519  wss 3560   class class class wbr 4618  cmpt 4678   × cxp 5077  wf 5846  ontowfo 5848  cfv 5850  cdom 7898  * cwdom 8407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-wdom 8409
This theorem is referenced by:  wdomd  8431  brwdom3  8432  unwdomg  8434  xpwdomg  8435  wdom2d2  37068
  Copyright terms: Public domain W3C validator