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

Theorem brwdom2 9400
Description: Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.)
Assertion
Ref Expression
brwdom2 (𝑌𝑉 → (𝑋* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋))
Distinct variable groups:   𝑦,𝑋,𝑧   𝑦,𝑌,𝑧
Allowed substitution hints:   𝑉(𝑦,𝑧)

Proof of Theorem brwdom2
Dummy variables 𝑥 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3459 . 2 (𝑌𝑉𝑌 ∈ V)
2 0wdom 9397 . . . . . 6 (𝑌 ∈ V → ∅ ≼* 𝑌)
3 breq1 5088 . . . . . 6 (𝑋 = ∅ → (𝑋* 𝑌 ↔ ∅ ≼* 𝑌))
42, 3syl5ibrcom 246 . . . . 5 (𝑌 ∈ V → (𝑋 = ∅ → 𝑋* 𝑌))
54imp 407 . . . 4 ((𝑌 ∈ V ∧ 𝑋 = ∅) → 𝑋* 𝑌)
6 0elpw 5291 . . . . . . 7 ∅ ∈ 𝒫 𝑌
7 f1o0 6788 . . . . . . . 8 ∅:∅–1-1-onto→∅
8 f1ofo 6758 . . . . . . . 8 (∅:∅–1-1-onto→∅ → ∅:∅–onto→∅)
9 0ex 5244 . . . . . . . . 9 ∅ ∈ V
10 foeq1 6719 . . . . . . . . 9 (𝑧 = ∅ → (𝑧:∅–onto→∅ ↔ ∅:∅–onto→∅))
119, 10spcev 3554 . . . . . . . 8 (∅:∅–onto→∅ → ∃𝑧 𝑧:∅–onto→∅)
127, 8, 11mp2b 10 . . . . . . 7 𝑧 𝑧:∅–onto→∅
13 foeq2 6720 . . . . . . . . 9 (𝑦 = ∅ → (𝑧:𝑦onto→∅ ↔ 𝑧:∅–onto→∅))
1413exbidv 1923 . . . . . . . 8 (𝑦 = ∅ → (∃𝑧 𝑧:𝑦onto→∅ ↔ ∃𝑧 𝑧:∅–onto→∅))
1514rspcev 3570 . . . . . . 7 ((∅ ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:∅–onto→∅) → ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto→∅)
166, 12, 15mp2an 689 . . . . . 6 𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto→∅
17 foeq3 6721 . . . . . . . 8 (𝑋 = ∅ → (𝑧:𝑦onto𝑋𝑧:𝑦onto→∅))
1817exbidv 1923 . . . . . . 7 (𝑋 = ∅ → (∃𝑧 𝑧:𝑦onto𝑋 ↔ ∃𝑧 𝑧:𝑦onto→∅))
1918rexbidv 3172 . . . . . 6 (𝑋 = ∅ → (∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto→∅))
2016, 19mpbiri 257 . . . . 5 (𝑋 = ∅ → ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋)
2120adantl 482 . . . 4 ((𝑌 ∈ V ∧ 𝑋 = ∅) → ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋)
225, 212thd 264 . . 3 ((𝑌 ∈ V ∧ 𝑋 = ∅) → (𝑋* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋))
23 brwdomn0 9396 . . . . 5 (𝑋 ≠ ∅ → (𝑋* 𝑌 ↔ ∃𝑥 𝑥:𝑌onto𝑋))
2423adantl 482 . . . 4 ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋* 𝑌 ↔ ∃𝑥 𝑥:𝑌onto𝑋))
25 foeq1 6719 . . . . . . 7 (𝑥 = 𝑧 → (𝑥:𝑌onto𝑋𝑧:𝑌onto𝑋))
2625cbvexvw 2039 . . . . . 6 (∃𝑥 𝑥:𝑌onto𝑋 ↔ ∃𝑧 𝑧:𝑌onto𝑋)
27 pwidg 4563 . . . . . . . . 9 (𝑌 ∈ V → 𝑌 ∈ 𝒫 𝑌)
2827ad2antrr 723 . . . . . . . 8 (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ ∃𝑧 𝑧:𝑌onto𝑋) → 𝑌 ∈ 𝒫 𝑌)
29 foeq2 6720 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑧:𝑦onto𝑋𝑧:𝑌onto𝑋))
3029exbidv 1923 . . . . . . . . 9 (𝑦 = 𝑌 → (∃𝑧 𝑧:𝑦onto𝑋 ↔ ∃𝑧 𝑧:𝑌onto𝑋))
3130rspcev 3570 . . . . . . . 8 ((𝑌 ∈ 𝒫 𝑌 ∧ ∃𝑧 𝑧:𝑌onto𝑋) → ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋)
3228, 31sylancom 588 . . . . . . 7 (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ ∃𝑧 𝑧:𝑌onto𝑋) → ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋)
3332ex 413 . . . . . 6 ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑧 𝑧:𝑌onto𝑋 → ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋))
3426, 33biimtrid 241 . . . . 5 ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑥 𝑥:𝑌onto𝑋 → ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋))
35 n0 4290 . . . . . . . . . . 11 (𝑋 ≠ ∅ ↔ ∃𝑤 𝑤𝑋)
3635biimpi 215 . . . . . . . . . 10 (𝑋 ≠ ∅ → ∃𝑤 𝑤𝑋)
3736ad2antlr 724 . . . . . . . . 9 (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) → ∃𝑤 𝑤𝑋)
38 vex 3445 . . . . . . . . . . . . 13 𝑧 ∈ V
39 difexg 5264 . . . . . . . . . . . . . 14 (𝑌 ∈ V → (𝑌𝑦) ∈ V)
40 snex 5367 . . . . . . . . . . . . . 14 {𝑤} ∈ V
41 xpexg 7638 . . . . . . . . . . . . . 14 (((𝑌𝑦) ∈ V ∧ {𝑤} ∈ V) → ((𝑌𝑦) × {𝑤}) ∈ V)
4239, 40, 41sylancl 586 . . . . . . . . . . . . 13 (𝑌 ∈ V → ((𝑌𝑦) × {𝑤}) ∈ V)
43 unexg 7637 . . . . . . . . . . . . 13 ((𝑧 ∈ V ∧ ((𝑌𝑦) × {𝑤}) ∈ V) → (𝑧 ∪ ((𝑌𝑦) × {𝑤})) ∈ V)
4438, 42, 43sylancr 587 . . . . . . . . . . . 12 (𝑌 ∈ V → (𝑧 ∪ ((𝑌𝑦) × {𝑤})) ∈ V)
4544adantr 481 . . . . . . . . . . 11 ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑧 ∪ ((𝑌𝑦) × {𝑤})) ∈ V)
4645ad2antrr 723 . . . . . . . . . 10 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (𝑧 ∪ ((𝑌𝑦) × {𝑤})) ∈ V)
47 fofn 6725 . . . . . . . . . . . . . . 15 (𝑧:𝑦onto𝑋𝑧 Fn 𝑦)
4847adantl 482 . . . . . . . . . . . . . 14 ((𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋) → 𝑧 Fn 𝑦)
4948ad2antlr 724 . . . . . . . . . . . . 13 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → 𝑧 Fn 𝑦)
50 vex 3445 . . . . . . . . . . . . . 14 𝑤 ∈ V
51 fnconstg 6697 . . . . . . . . . . . . . 14 (𝑤 ∈ V → ((𝑌𝑦) × {𝑤}) Fn (𝑌𝑦))
5250, 51mp1i 13 . . . . . . . . . . . . 13 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → ((𝑌𝑦) × {𝑤}) Fn (𝑌𝑦))
53 disjdif 4415 . . . . . . . . . . . . . 14 (𝑦 ∩ (𝑌𝑦)) = ∅
5453a1i 11 . . . . . . . . . . . . 13 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (𝑦 ∩ (𝑌𝑦)) = ∅)
5549, 52, 54fnund 6582 . . . . . . . . . . . 12 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (𝑧 ∪ ((𝑌𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌𝑦)))
56 elpwi 4550 . . . . . . . . . . . . . . . 16 (𝑦 ∈ 𝒫 𝑌𝑦𝑌)
57 undif 4425 . . . . . . . . . . . . . . . 16 (𝑦𝑌 ↔ (𝑦 ∪ (𝑌𝑦)) = 𝑌)
5856, 57sylib 217 . . . . . . . . . . . . . . 15 (𝑦 ∈ 𝒫 𝑌 → (𝑦 ∪ (𝑌𝑦)) = 𝑌)
5958ad2antrl 725 . . . . . . . . . . . . . 14 (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) → (𝑦 ∪ (𝑌𝑦)) = 𝑌)
6059adantr 481 . . . . . . . . . . . . 13 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (𝑦 ∪ (𝑌𝑦)) = 𝑌)
6160fneq2d 6563 . . . . . . . . . . . 12 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → ((𝑧 ∪ ((𝑌𝑦) × {𝑤})) Fn (𝑦 ∪ (𝑌𝑦)) ↔ (𝑧 ∪ ((𝑌𝑦) × {𝑤})) Fn 𝑌))
6255, 61mpbid 231 . . . . . . . . . . 11 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (𝑧 ∪ ((𝑌𝑦) × {𝑤})) Fn 𝑌)
63 rnun 6069 . . . . . . . . . . . 12 ran (𝑧 ∪ ((𝑌𝑦) × {𝑤})) = (ran 𝑧 ∪ ran ((𝑌𝑦) × {𝑤}))
64 forn 6726 . . . . . . . . . . . . . . . 16 (𝑧:𝑦onto𝑋 → ran 𝑧 = 𝑋)
6564ad2antll 726 . . . . . . . . . . . . . . 15 (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) → ran 𝑧 = 𝑋)
6665adantr 481 . . . . . . . . . . . . . 14 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → ran 𝑧 = 𝑋)
6766uneq1d 4106 . . . . . . . . . . . . 13 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (ran 𝑧 ∪ ran ((𝑌𝑦) × {𝑤})) = (𝑋 ∪ ran ((𝑌𝑦) × {𝑤})))
68 fconst6g 6698 . . . . . . . . . . . . . . . 16 (𝑤𝑋 → ((𝑌𝑦) × {𝑤}):(𝑌𝑦)⟶𝑋)
6968frnd 6643 . . . . . . . . . . . . . . 15 (𝑤𝑋 → ran ((𝑌𝑦) × {𝑤}) ⊆ 𝑋)
7069adantl 482 . . . . . . . . . . . . . 14 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → ran ((𝑌𝑦) × {𝑤}) ⊆ 𝑋)
71 ssequn2 4127 . . . . . . . . . . . . . 14 (ran ((𝑌𝑦) × {𝑤}) ⊆ 𝑋 ↔ (𝑋 ∪ ran ((𝑌𝑦) × {𝑤})) = 𝑋)
7270, 71sylib 217 . . . . . . . . . . . . 13 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (𝑋 ∪ ran ((𝑌𝑦) × {𝑤})) = 𝑋)
7367, 72eqtrd 2777 . . . . . . . . . . . 12 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (ran 𝑧 ∪ ran ((𝑌𝑦) × {𝑤})) = 𝑋)
7463, 73eqtrid 2789 . . . . . . . . . . 11 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → ran (𝑧 ∪ ((𝑌𝑦) × {𝑤})) = 𝑋)
75 df-fo 6469 . . . . . . . . . . 11 ((𝑧 ∪ ((𝑌𝑦) × {𝑤})):𝑌onto𝑋 ↔ ((𝑧 ∪ ((𝑌𝑦) × {𝑤})) Fn 𝑌 ∧ ran (𝑧 ∪ ((𝑌𝑦) × {𝑤})) = 𝑋))
7662, 74, 75sylanbrc 583 . . . . . . . . . 10 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → (𝑧 ∪ ((𝑌𝑦) × {𝑤})):𝑌onto𝑋)
77 foeq1 6719 . . . . . . . . . 10 (𝑥 = (𝑧 ∪ ((𝑌𝑦) × {𝑤})) → (𝑥:𝑌onto𝑋 ↔ (𝑧 ∪ ((𝑌𝑦) × {𝑤})):𝑌onto𝑋))
7846, 76, 77spcedv 3546 . . . . . . . . 9 ((((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) ∧ 𝑤𝑋) → ∃𝑥 𝑥:𝑌onto𝑋)
7937, 78exlimddv 1937 . . . . . . . 8 (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ (𝑦 ∈ 𝒫 𝑌𝑧:𝑦onto𝑋)) → ∃𝑥 𝑥:𝑌onto𝑋)
8079expr 457 . . . . . . 7 (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (𝑧:𝑦onto𝑋 → ∃𝑥 𝑥:𝑌onto𝑋))
8180exlimdv 1935 . . . . . 6 (((𝑌 ∈ V ∧ 𝑋 ≠ ∅) ∧ 𝑦 ∈ 𝒫 𝑌) → (∃𝑧 𝑧:𝑦onto𝑋 → ∃𝑥 𝑥:𝑌onto𝑋))
8281rexlimdva 3149 . . . . 5 ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋 → ∃𝑥 𝑥:𝑌onto𝑋))
8334, 82impbid 211 . . . 4 ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (∃𝑥 𝑥:𝑌onto𝑋 ↔ ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋))
8424, 83bitrd 278 . . 3 ((𝑌 ∈ V ∧ 𝑋 ≠ ∅) → (𝑋* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋))
8522, 84pm2.61dane 3030 . 2 (𝑌 ∈ V → (𝑋* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋))
861, 85syl 17 1 (𝑌𝑉 → (𝑋* 𝑌 ↔ ∃𝑦 ∈ 𝒫 𝑌𝑧 𝑧:𝑦onto𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wex 1780  wcel 2105  wne 2941  wrex 3071  Vcvv 3441  cdif 3893  cun 3894  cin 3895  wss 3896  c0 4266  𝒫 cpw 4543  {csn 4569   class class class wbr 5085   × cxp 5603  ran crn 5606   Fn wfn 6458  ontowfo 6461  1-1-ontowf1o 6462  * cwdom 9391
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-wdom 9392
This theorem is referenced by:  brwdom3  9409
  Copyright terms: Public domain W3C validator