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 36443
Description: Lemma for weiunfr 36446. (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 36442 . . . . . . . . 9 (𝜑 → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑠𝐴𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡)))
65simp1d 1143 . . . . . . . 8 (𝜑𝐹: 𝑥𝐴 𝐵𝐴)
76fimassd 6755 . . . . . . 7 (𝜑 → (𝐹𝑟) ⊆ 𝐴)
8 weiunfrlem.6 . . . . . . . . . . 11 (𝜑𝑟 𝑥𝐴 𝐵)
96fdmd 6744 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝑥𝐴 𝐵)
108, 9sseqtrrd 4020 . . . . . . . . . 10 (𝜑𝑟 ⊆ dom 𝐹)
11 sseqin2 4222 . . . . . . . . . 10 (𝑟 ⊆ dom 𝐹 ↔ (dom 𝐹𝑟) = 𝑟)
1210, 11sylib 218 . . . . . . . . 9 (𝜑 → (dom 𝐹𝑟) = 𝑟)
13 weiunfrlem.7 . . . . . . . . 9 (𝜑𝑟 ≠ ∅)
1412, 13eqnetrd 3007 . . . . . . . 8 (𝜑 → (dom 𝐹𝑟) ≠ ∅)
1514imadisjlnd 6097 . . . . . . 7 (𝜑 → (𝐹𝑟) ≠ ∅)
16 wereu2 5680 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ ((𝐹𝑟) ⊆ 𝐴 ∧ (𝐹𝑟) ≠ ∅)) → ∃!𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝)
171, 2, 7, 15, 16syl22anc 839 . . . . . 6 (𝜑 → ∃!𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝)
18 riotacl2 7402 . . . . . 6 (∃!𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝 → (𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝) ∈ {𝑝 ∈ (𝐹𝑟) ∣ ∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝})
1917, 18syl 17 . . . . 5 (𝜑 → (𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝) ∈ {𝑝 ∈ (𝐹𝑟) ∣ ∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝})
20 weiunfrlem.5 . . . . 5 𝐸 = (𝑝 ∈ (𝐹𝑟)∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝)
21 simpr 484 . . . . . . . . 9 ((𝑛 = 𝑝𝑜 = 𝑞) → 𝑜 = 𝑞)
22 simpl 482 . . . . . . . . 9 ((𝑛 = 𝑝𝑜 = 𝑞) → 𝑛 = 𝑝)
2321, 22breq12d 5154 . . . . . . . 8 ((𝑛 = 𝑝𝑜 = 𝑞) → (𝑜𝑅𝑛𝑞𝑅𝑝))
2423notbid 318 . . . . . . 7 ((𝑛 = 𝑝𝑜 = 𝑞) → (¬ 𝑜𝑅𝑛 ↔ ¬ 𝑞𝑅𝑝))
2524cbvraldva 3238 . . . . . 6 (𝑛 = 𝑝 → (∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛 ↔ ∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝))
2625cbvrabv 3446 . . . . 5 {𝑛 ∈ (𝐹𝑟) ∣ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛} = {𝑝 ∈ (𝐹𝑟) ∣ ∀𝑞 ∈ (𝐹𝑟) ¬ 𝑞𝑅𝑝}
2719, 20, 263eltr4g 2857 . . . 4 (𝜑𝐸 ∈ {𝑛 ∈ (𝐹𝑟) ∣ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛})
28 breq2 5145 . . . . . . 7 (𝑛 = 𝐸 → (𝑜𝑅𝑛𝑜𝑅𝐸))
2928notbid 318 . . . . . 6 (𝑛 = 𝐸 → (¬ 𝑜𝑅𝑛 ↔ ¬ 𝑜𝑅𝐸))
3029ralbidv 3177 . . . . 5 (𝑛 = 𝐸 → (∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛 ↔ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸))
3130elrab 3691 . . . 4 (𝐸 ∈ {𝑛 ∈ (𝐹𝑟) ∣ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝑛} ↔ (𝐸 ∈ (𝐹𝑟) ∧ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸))
3227, 31sylib 218 . . 3 (𝜑 → (𝐸 ∈ (𝐹𝑟) ∧ ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸))
3332simpld 494 . 2 (𝜑𝐸 ∈ (𝐹𝑟))
3432simprd 495 . . 3 (𝜑 → ∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸)
356ffnd 6735 . . . 4 (𝜑𝐹 Fn 𝑥𝐴 𝐵)
36 breq1 5144 . . . . . 6 (𝑜 = (𝐹𝑡) → (𝑜𝑅𝐸 ↔ (𝐹𝑡)𝑅𝐸))
3736notbid 318 . . . . 5 (𝑜 = (𝐹𝑡) → (¬ 𝑜𝑅𝐸 ↔ ¬ (𝐹𝑡)𝑅𝐸))
3837ralima 7255 . . . 4 ((𝐹 Fn 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵) → (∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸 ↔ ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸))
3935, 8, 38syl2anc 584 . . 3 (𝜑 → (∀𝑜 ∈ (𝐹𝑟) ¬ 𝑜𝑅𝐸 ↔ ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸))
4034, 39mpbid 232 . 2 (𝜑 → ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸)
41 simpr 484 . . . . . 6 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑡 ∈ (𝑟𝐸 / 𝑥𝐵))
4241elin1d 4203 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑡𝑟)
43 rspa 3247 . . . . 5 ((∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸𝑡𝑟) → ¬ (𝐹𝑡)𝑅𝐸)
4440, 42, 43syl2an2r 685 . . . 4 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → ¬ (𝐹𝑡)𝑅𝐸)
45 csbeq1 3901 . . . . . . 7 (𝑠 = 𝐸𝑠 / 𝑥𝐵 = 𝐸 / 𝑥𝐵)
46 breq1 5144 . . . . . . . 8 (𝑠 = 𝐸 → (𝑠𝑅(𝐹𝑡) ↔ 𝐸𝑅(𝐹𝑡)))
4746notbid 318 . . . . . . 7 (𝑠 = 𝐸 → (¬ 𝑠𝑅(𝐹𝑡) ↔ ¬ 𝐸𝑅(𝐹𝑡)))
4845, 47raleqbidv 3345 . . . . . 6 (𝑠 = 𝐸 → (∀𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡) ↔ ∀𝑡 𝐸 / 𝑥𝐵 ¬ 𝐸𝑅(𝐹𝑡)))
495simp3d 1145 . . . . . 6 (𝜑 → ∀𝑠𝐴𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡))
507, 33sseldd 3983 . . . . . 6 (𝜑𝐸𝐴)
5148, 49, 50rspcdva 3622 . . . . 5 (𝜑 → ∀𝑡 𝐸 / 𝑥𝐵 ¬ 𝐸𝑅(𝐹𝑡))
5241elin2d 4204 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑡𝐸 / 𝑥𝐵)
53 rspa 3247 . . . . 5 ((∀𝑡 𝐸 / 𝑥𝐵 ¬ 𝐸𝑅(𝐹𝑡) ∧ 𝑡𝐸 / 𝑥𝐵) → ¬ 𝐸𝑅(𝐹𝑡))
5451, 52, 53syl2an2r 685 . . . 4 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → ¬ 𝐸𝑅(𝐹𝑡))
55 weso 5674 . . . . . . 7 (𝑅 We 𝐴𝑅 Or 𝐴)
561, 55syl 17 . . . . . 6 (𝜑𝑅 Or 𝐴)
5756adantr 480 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑅 Or 𝐴)
586adantr 480 . . . . . 6 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝐹: 𝑥𝐴 𝐵𝐴)
598adantr 480 . . . . . . 7 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑟 𝑥𝐴 𝐵)
6059, 42sseldd 3983 . . . . . 6 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝑡 𝑥𝐴 𝐵)
6158, 60ffvelcdmd 7103 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → (𝐹𝑡) ∈ 𝐴)
6250adantr 480 . . . . 5 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → 𝐸𝐴)
63 sotrieq2 5622 . . . . 5 ((𝑅 Or 𝐴 ∧ ((𝐹𝑡) ∈ 𝐴𝐸𝐴)) → ((𝐹𝑡) = 𝐸 ↔ (¬ (𝐹𝑡)𝑅𝐸 ∧ ¬ 𝐸𝑅(𝐹𝑡))))
6457, 61, 62, 63syl12anc 837 . . . 4 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → ((𝐹𝑡) = 𝐸 ↔ (¬ (𝐹𝑡)𝑅𝐸 ∧ ¬ 𝐸𝑅(𝐹𝑡))))
6544, 54, 64mpbir2and 713 . . 3 ((𝜑𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)) → (𝐹𝑡) = 𝐸)
6665ralrimiva 3145 . 2 (𝜑 → ∀𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)(𝐹𝑡) = 𝐸)
6733, 40, 663jca 1129 1 (𝜑 → (𝐸 ∈ (𝐹𝑟) ∧ ∀𝑡𝑟 ¬ (𝐹𝑡)𝑅𝐸 ∧ ∀𝑡 ∈ (𝑟𝐸 / 𝑥𝐵)(𝐹𝑡) = 𝐸))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wne 2939  wral 3060  ∃!wreu 3377  {crab 3435  csb 3898  cin 3949  wss 3950  c0 4332   ciun 4989   class class class wbr 5141  {copab 5203  cmpt 5223   Or wor 5589   Se wse 5633   We wwe 5634  dom cdm 5683  cima 5686   Fn wfn 6554  wf 6555  cfv 6559  crio 7385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5294  ax-nul 5304  ax-pr 5430
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  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 6512  df-fun 6561  df-fn 6562  df-f 6563  df-fv 6567  df-riota 7386
This theorem is referenced by:  weiunfr  36446
  Copyright terms: Public domain W3C validator