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

Theorem ustuqtop1 24266
Description: Lemma for ustuqtop 24271, similar to ssnei2 23140. (Contributed by Thierry Arnoux, 11-Jan-2018.)
Hypothesis
Ref Expression
utopustuq.1 𝑁 = (𝑝𝑋 ↦ ran (𝑣𝑈 ↦ (𝑣 “ {𝑝})))
Assertion
Ref Expression
ustuqtop1 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝))
Distinct variable groups:   𝑣,𝑝,𝑈   𝑋,𝑝,𝑣   𝑎,𝑏,𝑝,𝑁   𝑣,𝑎,𝑈,𝑏   𝑋,𝑎,𝑏
Allowed substitution hint:   𝑁(𝑣)

Proof of Theorem ustuqtop1
Dummy variables 𝑤 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl1l 1223 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ (𝑎 ∈ (𝑁𝑝) ∧ 𝑤𝑈𝑎 = (𝑤 “ {𝑝}))) → 𝑈 ∈ (UnifOn‘𝑋))
213anassrs 1359 . . . . 5 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑈 ∈ (UnifOn‘𝑋))
3 simplr 769 . . . . 5 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑤𝑈)
4 ustssxp 24229 . . . . . . 7 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈) → 𝑤 ⊆ (𝑋 × 𝑋))
52, 3, 4syl2anc 584 . . . . . 6 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑤 ⊆ (𝑋 × 𝑋))
6 simpl1r 1224 . . . . . . . . 9 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ (𝑎 ∈ (𝑁𝑝) ∧ 𝑤𝑈𝑎 = (𝑤 “ {𝑝}))) → 𝑝𝑋)
763anassrs 1359 . . . . . . . 8 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑝𝑋)
87snssd 4814 . . . . . . 7 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → {𝑝} ⊆ 𝑋)
9 simpl3 1192 . . . . . . . 8 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ (𝑎 ∈ (𝑁𝑝) ∧ 𝑤𝑈𝑎 = (𝑤 “ {𝑝}))) → 𝑏𝑋)
1093anassrs 1359 . . . . . . 7 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑏𝑋)
11 xpss12 5704 . . . . . . 7 (({𝑝} ⊆ 𝑋𝑏𝑋) → ({𝑝} × 𝑏) ⊆ (𝑋 × 𝑋))
128, 10, 11syl2anc 584 . . . . . 6 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ({𝑝} × 𝑏) ⊆ (𝑋 × 𝑋))
135, 12unssd 4202 . . . . 5 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (𝑤 ∪ ({𝑝} × 𝑏)) ⊆ (𝑋 × 𝑋))
14 ssun1 4188 . . . . . 6 𝑤 ⊆ (𝑤 ∪ ({𝑝} × 𝑏))
1514a1i 11 . . . . 5 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑤 ⊆ (𝑤 ∪ ({𝑝} × 𝑏)))
16 ustssel 24230 . . . . . 6 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈 ∧ (𝑤 ∪ ({𝑝} × 𝑏)) ⊆ (𝑋 × 𝑋)) → (𝑤 ⊆ (𝑤 ∪ ({𝑝} × 𝑏)) → (𝑤 ∪ ({𝑝} × 𝑏)) ∈ 𝑈))
1716imp 406 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑤𝑈 ∧ (𝑤 ∪ ({𝑝} × 𝑏)) ⊆ (𝑋 × 𝑋)) ∧ 𝑤 ⊆ (𝑤 ∪ ({𝑝} × 𝑏))) → (𝑤 ∪ ({𝑝} × 𝑏)) ∈ 𝑈)
182, 3, 13, 15, 17syl31anc 1372 . . . 4 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → (𝑤 ∪ ({𝑝} × 𝑏)) ∈ 𝑈)
19 simpl2 1191 . . . . . 6 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ (𝑎 ∈ (𝑁𝑝) ∧ 𝑤𝑈𝑎 = (𝑤 “ {𝑝}))) → 𝑎𝑏)
20193anassrs 1359 . . . . 5 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑎𝑏)
21 ssequn1 4196 . . . . . . 7 (𝑎𝑏 ↔ (𝑎𝑏) = 𝑏)
2221biimpi 216 . . . . . 6 (𝑎𝑏 → (𝑎𝑏) = 𝑏)
23 id 22 . . . . . . . 8 (𝑎 = (𝑤 “ {𝑝}) → 𝑎 = (𝑤 “ {𝑝}))
24 inidm 4235 . . . . . . . . . . 11 ({𝑝} ∩ {𝑝}) = {𝑝}
25 vex 3482 . . . . . . . . . . . 12 𝑝 ∈ V
2625snnz 4781 . . . . . . . . . . 11 {𝑝} ≠ ∅
2724, 26eqnetri 3009 . . . . . . . . . 10 ({𝑝} ∩ {𝑝}) ≠ ∅
28 xpima2 6206 . . . . . . . . . 10 (({𝑝} ∩ {𝑝}) ≠ ∅ → (({𝑝} × 𝑏) “ {𝑝}) = 𝑏)
2927, 28mp1i 13 . . . . . . . . 9 (𝑎 = (𝑤 “ {𝑝}) → (({𝑝} × 𝑏) “ {𝑝}) = 𝑏)
3029eqcomd 2741 . . . . . . . 8 (𝑎 = (𝑤 “ {𝑝}) → 𝑏 = (({𝑝} × 𝑏) “ {𝑝}))
3123, 30uneq12d 4179 . . . . . . 7 (𝑎 = (𝑤 “ {𝑝}) → (𝑎𝑏) = ((𝑤 “ {𝑝}) ∪ (({𝑝} × 𝑏) “ {𝑝})))
32 imaundir 6173 . . . . . . 7 ((𝑤 ∪ ({𝑝} × 𝑏)) “ {𝑝}) = ((𝑤 “ {𝑝}) ∪ (({𝑝} × 𝑏) “ {𝑝}))
3331, 32eqtr4di 2793 . . . . . 6 (𝑎 = (𝑤 “ {𝑝}) → (𝑎𝑏) = ((𝑤 ∪ ({𝑝} × 𝑏)) “ {𝑝}))
3422, 33sylan9req 2796 . . . . 5 ((𝑎𝑏𝑎 = (𝑤 “ {𝑝})) → 𝑏 = ((𝑤 ∪ ({𝑝} × 𝑏)) “ {𝑝}))
3520, 34sylancom 588 . . . 4 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → 𝑏 = ((𝑤 ∪ ({𝑝} × 𝑏)) “ {𝑝}))
36 imaeq1 6075 . . . . 5 (𝑢 = (𝑤 ∪ ({𝑝} × 𝑏)) → (𝑢 “ {𝑝}) = ((𝑤 ∪ ({𝑝} × 𝑏)) “ {𝑝}))
3736rspceeqv 3645 . . . 4 (((𝑤 ∪ ({𝑝} × 𝑏)) ∈ 𝑈𝑏 = ((𝑤 ∪ ({𝑝} × 𝑏)) “ {𝑝})) → ∃𝑢𝑈 𝑏 = (𝑢 “ {𝑝}))
3818, 35, 37syl2anc 584 . . 3 ((((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) ∧ 𝑤𝑈) ∧ 𝑎 = (𝑤 “ {𝑝})) → ∃𝑢𝑈 𝑏 = (𝑢 “ {𝑝}))
39 utopustuq.1 . . . . . . 7 𝑁 = (𝑝𝑋 ↦ ran (𝑣𝑈 ↦ (𝑣 “ {𝑝})))
4039ustuqtoplem 24264 . . . . . 6 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ V) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
4140elvd 3484 . . . . 5 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) → (𝑎 ∈ (𝑁𝑝) ↔ ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝})))
4241biimpa 476 . . . 4 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝}))
43423ad2antl1 1184 . . 3 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑤𝑈 𝑎 = (𝑤 “ {𝑝}))
4438, 43r19.29a 3160 . 2 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → ∃𝑢𝑈 𝑏 = (𝑢 “ {𝑝}))
4539ustuqtoplem 24264 . . . . 5 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑏 ∈ V) → (𝑏 ∈ (𝑁𝑝) ↔ ∃𝑢𝑈 𝑏 = (𝑢 “ {𝑝})))
4645elvd 3484 . . . 4 ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) → (𝑏 ∈ (𝑁𝑝) ↔ ∃𝑢𝑈 𝑏 = (𝑢 “ {𝑝})))
47463ad2ant1 1132 . . 3 (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) → (𝑏 ∈ (𝑁𝑝) ↔ ∃𝑢𝑈 𝑏 = (𝑢 “ {𝑝})))
4847adantr 480 . 2 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → (𝑏 ∈ (𝑁𝑝) ↔ ∃𝑢𝑈 𝑏 = (𝑢 “ {𝑝})))
4944, 48mpbird 257 1 ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝𝑋) ∧ 𝑎𝑏𝑏𝑋) ∧ 𝑎 ∈ (𝑁𝑝)) → 𝑏 ∈ (𝑁𝑝))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wrex 3068  Vcvv 3478  cun 3961  cin 3962  wss 3963  c0 4339  {csn 4631  cmpt 5231   × cxp 5687  ran crn 5690  cima 5692  cfv 6563  UnifOncust 24224
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ust 24225
This theorem is referenced by:  ustuqtop4  24269  ustuqtop  24271  utopsnneiplem  24272
  Copyright terms: Public domain W3C validator