Users' Mathboxes Mathbox for Matthew House < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  weiunfrlem Structured version   Visualization version   GIF version

Theorem weiunfrlem 36407
Description: Lemma for weiunfr 36410. (Contributed by Matthew House, 23-Aug-2025.)
Hypotheses
Ref Expression
weiun.1 𝐹 = (𝑤 𝑥𝐴 𝐵 ↦ (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢))
weiun.2 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵) ∧ ((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)))}
weiunlem2.3 (𝜑𝑅 We 𝐴)
weiunlem2.4 (𝜑𝑅 Se 𝐴)
weiunfrlem.5 𝐸 = (𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝)
weiunfrlem.6 (𝜑𝑟 𝑥𝐴 𝐵)
weiunfrlem.7 (𝜑𝑟 ≠ ∅)
Assertion
Ref Expression
weiunfrlem (𝜑 → (𝐸 ∈ (𝐹𝑟) ∧ ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸 ∧ ∀𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)(𝐹𝑡) = 𝐸))
Distinct variable groups:   𝜑,𝑡   𝐴,𝑝,𝑞,𝑟,𝑡,𝑢,𝑣,𝑤,𝑥   𝑦,𝐴,𝑧,𝑥   𝐵,𝑝,𝑞,𝑟,𝑡,𝑢,𝑣,𝑤   𝑦,𝐵,𝑧   𝑡,𝐸   𝐹,𝑝,𝑞,𝑟,𝑡,𝑦,𝑧   𝑅,𝑝,𝑞,𝑟,𝑡,𝑢,𝑣,𝑤   𝑦,𝑅,𝑧   𝑆,𝑝,𝑞,𝑟,𝑡,𝑦,𝑧   𝑇,𝑝,𝑞,𝑟
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑟,𝑞,𝑝)   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥,𝑤,𝑣,𝑢)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑡)   𝐸(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑟,𝑞,𝑝)   𝐹(𝑥,𝑤,𝑣,𝑢)

Proof of Theorem weiunfrlem
Dummy variables 𝑛 𝑜 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 weiunlem2.3 . . . . . . 7 (𝜑𝑅 We 𝐴)
2 weiunlem2.4 . . . . . . 7 (𝜑𝑅 Se 𝐴)
3 weiun.1 . . . . . . . . . 10 𝐹 = (𝑤 𝑥𝐴 𝐵 ↦ (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢))
4 weiun.2 . . . . . . . . . 10 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵) ∧ ((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)))}
53, 4, 1, 2weiunlem2 36406 . . . . . . . . 9 (𝜑 → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑠𝐴𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡)))
65simp1d 1140 . . . . . . . 8 (𝜑𝐹: 𝑥𝐴 𝐵𝐴)
76fimassd 6752 . . . . . . 7 (𝜑 → (𝐹𝑟) ⊆ 𝐴)
8 weiunfrlem.6 . . . . . . . . . . 11 (𝜑𝑟 𝑥𝐴 𝐵)
96fdmd 6741 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝑥𝐴 𝐵)
108, 9sseqtrrd 4037 . . . . . . . . . 10 (𝜑𝑟 ⊆ dom 𝐹)
11 sseqin2 4231 . . . . . . . . . 10 (𝑟 ⊆ dom 𝐹 ↔ (dom 𝐹𝑟) = 𝑟)
1210, 11sylib 218 . . . . . . . . 9 (𝜑 → (dom 𝐹𝑟) = 𝑟)
13 weiunfrlem.7 . . . . . . . . 9 (𝜑𝑟 ≠ ∅)
1412, 13eqnetrd 3004 . . . . . . . 8 (𝜑 → (dom 𝐹𝑟) ≠ ∅)
1514imadisjlnd 6095 . . . . . . 7 (𝜑 → (𝐹𝑟) ≠ ∅)
16 wereu2 5680 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ ((𝐹𝑟) ⊆ 𝐴 ∧ (𝐹𝑟) ≠ ∅)) → ∃!𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝)
171, 2, 7, 15, 16syl22anc 838 . . . . . 6 (𝜑 → ∃!𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝)
18 riotacl2 7398 . . . . . 6 (∃!𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝 → (𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝) ∈ {𝑝 ∈ (𝐹𝑟) ∣ ∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝})
1917, 18syl 17 . . . . 5 (𝜑 → (𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝) ∈ {𝑝 ∈ (𝐹𝑟) ∣ ∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝})
20 weiunfrlem.5 . . . . 5 𝐸 = (𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝)
21 simpr 484 . . . . . . . . 9 ((𝑛 = 𝑝𝑜 = 𝑞) → 𝑜 = 𝑞)
22 simpl 482 . . . . . . . . 9 ((𝑛 = 𝑝𝑜 = 𝑞) → 𝑛 = 𝑝)
2321, 22breq12d 5162 . . . . . . . 8 ((𝑛 = 𝑝𝑜 = 𝑞) → (𝑜𝑅𝑛𝑞𝑅𝑝))
2423notbid 318 . . . . . . 7 ((𝑛 = 𝑝𝑜 = 𝑞) → (¬ 𝑜𝑅𝑛 ↔ ¬ 𝑞𝑅𝑝))
2524cbvraldva 3235 . . . . . 6 (𝑛 = 𝑝 → (∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛 ↔ ∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝))
2625cbvrabv 3443 . . . . 5 {𝑛 ∈ (𝐹𝑟) ∣ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛} = {𝑝 ∈ (𝐹𝑟) ∣ ∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝}
2719, 20, 263eltr4g 2854 . . . 4 (𝜑𝐸 ∈ {𝑛 ∈ (𝐹𝑟) ∣ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛})
28 breq2 5153 . . . . . . 7 (𝑛 = 𝐸 → (𝑜𝑅𝑛𝑜𝑅𝐸))
2928notbid 318 . . . . . 6 (𝑛 = 𝐸 → (¬ 𝑜𝑅𝑛 ↔ ¬ 𝑜𝑅𝐸))
3029ralbidv 3174 . . . . 5 (𝑛 = 𝐸 → (∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛 ↔ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸))
3130elrab 3695 . . . 4 (𝐸 ∈ {𝑛 ∈ (𝐹𝑟) ∣ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛} ↔ (𝐸 ∈ (𝐹𝑟) ∧ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸))
3227, 31sylib 218 . . 3 (𝜑 → (𝐸 ∈ (𝐹𝑟) ∧ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸))
3332simpld 494 . 2 (𝜑𝐸 ∈ (𝐹𝑟))
3432simprd 495 . . 3 (𝜑 → ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸)
356ffnd 6732 . . . 4 (𝜑𝐹 Fn 𝑥𝐴 𝐵)
36 breq1 5152 . . . . . 6 (𝑜 = (𝐹𝑡) → (𝑜𝑅𝐸 ↔ (𝐹𝑡)𝑅𝐸))
3736notbid 318 . . . . 5 (𝑜 = (𝐹𝑡) → (¬ 𝑜𝑅𝐸 ↔ ¬ (𝐹𝑡)𝑅𝐸))
3837ralima 7251 . . . 4 ((𝐹 Fn 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵) → (∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸 ↔ ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸))
3935, 8, 38syl2anc 583 . . 3 (𝜑 → (∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸 ↔ ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸))
4034, 39mpbid 232 . 2 (𝜑 → ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸)
41 simpr 484 . . . . . 6 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑡 ∈ (𝑟𝐸 / 𝑥𝐵))
4241elin1d 4214 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑡𝑟)
43 rspa 3244 . . . . 5 ((∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸𝑡𝑟) → ¬ (𝐹𝑡)𝑅𝐸)
4440, 42, 43syl2an2r 684 . . . 4 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → ¬ (𝐹𝑡)𝑅𝐸)
45 csbeq1 3911 . . . . . . 7 (𝑠 = 𝐸𝑠 / 𝑥𝐵 = 𝐸 / 𝑥𝐵)
46 breq1 5152 . . . . . . . 8 (𝑠 = 𝐸 → (𝑠𝑅(𝐹𝑡) ↔ 𝐸𝑅(𝐹𝑡)))
4746notbid 318 . . . . . . 7 (𝑠 = 𝐸 → (¬ 𝑠𝑅(𝐹𝑡) ↔ ¬ 𝐸𝑅(𝐹𝑡)))
4845, 47raleqbidv 3342 . . . . . 6 (𝑠 = 𝐸 → (∀𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡) ↔ ∀𝑡 𝐸 / 𝑥𝐵 ¬ 𝐸𝑅(𝐹𝑡)))
495simp3d 1142 . . . . . 6 (𝜑 → ∀𝑠𝐴𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡))
507, 33sseldd 3996 . . . . . 6 (𝜑𝐸𝐴)
5148, 49, 50rspcdva 3623 . . . . 5 (𝜑 → ∀𝑡 𝐸 / 𝑥𝐵 ¬ 𝐸𝑅(𝐹𝑡))
5241elin2d 4215 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑡𝐸 / 𝑥𝐵)
53 rspa 3244 . . . . 5 ((∀𝑡 𝐸 / 𝑥𝐵 ¬ 𝐸𝑅(𝐹𝑡) ∧ 𝑡𝐸 / 𝑥𝐵) → ¬ 𝐸𝑅(𝐹𝑡))
5451, 52, 53syl2an2r 684 . . . 4 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → ¬ 𝐸𝑅(𝐹𝑡))
55 weso 5674 . . . . . . 7 (𝑅 We 𝐴𝑅 Or 𝐴)
561, 55syl 17 . . . . . 6 (𝜑𝑅 Or 𝐴)
5756adantr 480 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑅 Or 𝐴)
586adantr 480 . . . . . 6 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝐹: 𝑥𝐴 𝐵𝐴)
598adantr 480 . . . . . . 7 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑟 𝑥𝐴 𝐵)
6059, 42sseldd 3996 . . . . . 6 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑡 𝑥𝐴 𝐵)
6158, 60ffvelcdmd 7099 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → (𝐹𝑡) ∈ 𝐴)
6250adantr 480 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝐸𝐴)
63 sotrieq2 5622 . . . . 5 ((𝑅 Or 𝐴 ∧ ((𝐹𝑡) ∈ 𝐴𝐸𝐴)) → ((𝐹𝑡) = 𝐸 ↔ (¬ (𝐹𝑡)𝑅𝐸 ∧ ¬ 𝐸𝑅(𝐹𝑡))))
6457, 61, 62, 63syl12anc 836 . . . 4 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → ((𝐹𝑡) = 𝐸 ↔ (¬ (𝐹𝑡)𝑅𝐸 ∧ ¬ 𝐸𝑅(𝐹𝑡))))
6544, 54, 64mpbir2and 712 . . 3 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → (𝐹𝑡) = 𝐸)
6665ralrimiva 3142 . 2 (𝜑 → ∀𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)(𝐹𝑡) = 𝐸)
6733, 40, 663jca 1126 1 (𝜑 → (𝐸 ∈ (𝐹𝑟) ∧ ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸 ∧ ∀𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)(𝐹𝑡) = 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 846  w3a 1085   = wceq 1535  wcel 2104  wne 2936  wral 3057  ∃!wreu 3374  {crab 3432  csb 3908  cin 3962  wss 3963  c0 4339   ciun 4998   class class class wbr 5149  {copab 5211  cmpt 5232   Or wor 5589   Se wse 5633   We wwe 5634  dom cdm 5683  cima 5686   Fn wfn 6553  wf 6554  cfv 6558  crio 7380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-10 2137  ax-11 2153  ax-12 2173  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5430
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2536  df-eu 2565  df-clab 2711  df-cleq 2725  df-clel 2812  df-nfc 2888  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3479  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4915  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-fr 5635  df-se 5636  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-riota 7381
This theorem is referenced by:  weiunfr  36410
  Copyright terms: Public domain W3C validator