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

Theorem weiunlem2 36429
Description: Lemma for weiunpo 36431, weiunso 36432, weiunfr 36433, and weiunse 36434. (Contributed by Matthew House, 23-Aug-2025.)
Hypotheses
Ref Expression
weiun.1 𝐹 = (𝑤 𝑥𝐴 𝐵 ↦ (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢))
weiun.2 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵) ∧ ((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)))}
weiunlem2.3 (𝜑𝑅 We 𝐴)
weiunlem2.4 (𝜑𝑅 Se 𝐴)
Assertion
Ref Expression
weiunlem2 (𝜑 → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑠𝐴𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡)))
Distinct variable groups:   𝜑,𝑡   𝐴,𝑠,𝑡,𝑢,𝑣,𝑤,𝑥   𝑦,𝐴,𝑧,𝑥   𝐵,𝑠,𝑡,𝑢,𝑣,𝑤   𝑦,𝐵,𝑧   𝐹,𝑠,𝑡,𝑦,𝑧   𝑅,𝑠,𝑡,𝑢,𝑣,𝑤   𝑦,𝑅,𝑧   𝑆,𝑠,𝑡,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑠)   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥,𝑤,𝑣,𝑢)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑡,𝑠)   𝐹(𝑥,𝑤,𝑣,𝑢)

Proof of Theorem weiunlem2
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 weiunlem2.3 . 2 (𝜑𝑅 We 𝐴)
2 weiunlem2.4 . 2 (𝜑𝑅 Se 𝐴)
3 riotaex 7408 . . . . . 6 (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢) ∈ V
4 weiun.1 . . . . . 6 𝐹 = (𝑤 𝑥𝐴 𝐵 ↦ (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢))
53, 4fnmpti 6723 . . . . 5 𝐹 Fn 𝑥𝐴 𝐵
65a1i 11 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴) → 𝐹 Fn 𝑥𝐴 𝐵)
7 breq2 5170 . . . . . . . . . . . . 13 (𝑢 = 𝑟 → (𝑣𝑅𝑢𝑣𝑅𝑟))
87notbid 318 . . . . . . . . . . . 12 (𝑢 = 𝑟 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑟))
98ralbidv 3184 . . . . . . . . . . 11 (𝑢 = 𝑟 → (∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑟))
109cbvriotavw 7414 . . . . . . . . . 10 (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢) = (𝑟 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑟)
11 eleq1w 2827 . . . . . . . . . . . 12 (𝑤 = 𝑡 → (𝑤𝐵𝑡𝐵))
1211rabbidv 3451 . . . . . . . . . . 11 (𝑤 = 𝑡 → {𝑥𝐴𝑤𝐵} = {𝑥𝐴𝑡𝐵})
13 breq1 5169 . . . . . . . . . . . . . 14 (𝑣 = 𝑠 → (𝑣𝑅𝑟𝑠𝑅𝑟))
1413notbid 318 . . . . . . . . . . . . 13 (𝑣 = 𝑠 → (¬ 𝑣𝑅𝑟 ↔ ¬ 𝑠𝑅𝑟))
1514cbvralvw 3243 . . . . . . . . . . . 12 (∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑟 ↔ ∀𝑠 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑠𝑅𝑟)
1612raleqdv 3334 . . . . . . . . . . . 12 (𝑤 = 𝑡 → (∀𝑠 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑠𝑅𝑟 ↔ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟))
1715, 16bitrid 283 . . . . . . . . . . 11 (𝑤 = 𝑡 → (∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑟 ↔ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟))
1812, 17riotaeqbidv 7407 . . . . . . . . . 10 (𝑤 = 𝑡 → (𝑟 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑟) = (𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟))
1910, 18eqtrid 2792 . . . . . . . . 9 (𝑤 = 𝑡 → (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢) = (𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟))
2019, 4, 3fvmpt3i 7034 . . . . . . . 8 (𝑡 𝑥𝐴 𝐵 → (𝐹𝑡) = (𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟))
2120adantl 481 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑡 𝑥𝐴 𝐵) → (𝐹𝑡) = (𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟))
22 eliun 5019 . . . . . . . . . 10 (𝑡 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑡𝐵)
23 rabn0 4412 . . . . . . . . . 10 ({𝑥𝐴𝑡𝐵} ≠ ∅ ↔ ∃𝑥𝐴 𝑡𝐵)
2422, 23bitr4i 278 . . . . . . . . 9 (𝑡 𝑥𝐴 𝐵 ↔ {𝑥𝐴𝑡𝐵} ≠ ∅)
25 ssrab2 4103 . . . . . . . . . 10 {𝑥𝐴𝑡𝐵} ⊆ 𝐴
26 wereu2 5697 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ ({𝑥𝐴𝑡𝐵} ⊆ 𝐴 ∧ {𝑥𝐴𝑡𝐵} ≠ ∅)) → ∃!𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟)
2725, 26mpanr1 702 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ {𝑥𝐴𝑡𝐵} ≠ ∅) → ∃!𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟)
2824, 27sylan2b 593 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑡 𝑥𝐴 𝐵) → ∃!𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟)
29 riotacl2 7421 . . . . . . . 8 (∃!𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟 → (𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟) ∈ {𝑟 ∈ {𝑥𝐴𝑡𝐵} ∣ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟})
3028, 29syl 17 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑡 𝑥𝐴 𝐵) → (𝑟 ∈ {𝑥𝐴𝑡𝐵}∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟) ∈ {𝑟 ∈ {𝑥𝐴𝑡𝐵} ∣ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟})
3121, 30eqeltrd 2844 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑡 𝑥𝐴 𝐵) → (𝐹𝑡) ∈ {𝑟 ∈ {𝑥𝐴𝑡𝐵} ∣ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟})
32 elrabi 3703 . . . . . 6 ((𝐹𝑡) ∈ {𝑟 ∈ {𝑥𝐴𝑡𝐵} ∣ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟} → (𝐹𝑡) ∈ {𝑥𝐴𝑡𝐵})
33 elrabi 3703 . . . . . 6 ((𝐹𝑡) ∈ {𝑥𝐴𝑡𝐵} → (𝐹𝑡) ∈ 𝐴)
3431, 32, 333syl 18 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑡 𝑥𝐴 𝐵) → (𝐹𝑡) ∈ 𝐴)
3534ralrimiva 3152 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑡 𝑥𝐴 𝐵(𝐹𝑡) ∈ 𝐴)
36 ffnfv 7153 . . . 4 (𝐹: 𝑥𝐴 𝐵𝐴 ↔ (𝐹 Fn 𝑥𝐴 𝐵 ∧ ∀𝑡 𝑥𝐴 𝐵(𝐹𝑡) ∈ 𝐴))
376, 35, 36sylanbrc 582 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴) → 𝐹: 𝑥𝐴 𝐵𝐴)
38 dfsbcq 3806 . . . . . . 7 (𝑠 = (𝐹𝑡) → ([𝑠 / 𝑥]𝑡𝐵[(𝐹𝑡) / 𝑥]𝑡𝐵))
39 nfcv 2908 . . . . . . . . 9 𝑥𝐴
4039elrabsf 3853 . . . . . . . 8 (𝑠 ∈ {𝑥𝐴𝑡𝐵} ↔ (𝑠𝐴[𝑠 / 𝑥]𝑡𝐵))
4140simprbi 496 . . . . . . 7 (𝑠 ∈ {𝑥𝐴𝑡𝐵} → [𝑠 / 𝑥]𝑡𝐵)
4238, 41vtoclga 3589 . . . . . 6 ((𝐹𝑡) ∈ {𝑥𝐴𝑡𝐵} → [(𝐹𝑡) / 𝑥]𝑡𝐵)
4331, 32, 423syl 18 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑡 𝑥𝐴 𝐵) → [(𝐹𝑡) / 𝑥]𝑡𝐵)
44 sbcel2 4441 . . . . 5 ([(𝐹𝑡) / 𝑥]𝑡𝐵𝑡(𝐹𝑡) / 𝑥𝐵)
4543, 44sylib 218 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑡 𝑥𝐴 𝐵) → 𝑡(𝐹𝑡) / 𝑥𝐵)
4645ralrimiva 3152 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵)
47 simpr 484 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝑠𝐴𝑡𝑠 / 𝑥𝐵)) → (𝑠𝐴𝑡𝑠 / 𝑥𝐵))
48 sbcel2 4441 . . . . . . . . . . 11 ([𝑠 / 𝑥]𝑡𝐵𝑡𝑠 / 𝑥𝐵)
4948anbi2i 622 . . . . . . . . . 10 ((𝑠𝐴[𝑠 / 𝑥]𝑡𝐵) ↔ (𝑠𝐴𝑡𝑠 / 𝑥𝐵))
5040, 49bitri 275 . . . . . . . . 9 (𝑠 ∈ {𝑥𝐴𝑡𝐵} ↔ (𝑠𝐴𝑡𝑠 / 𝑥𝐵))
5147, 50sylibr 234 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝑠𝐴𝑡𝑠 / 𝑥𝐵)) → 𝑠 ∈ {𝑥𝐴𝑡𝐵})
5251ne0d 4365 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝑠𝐴𝑡𝑠 / 𝑥𝐵)) → {𝑥𝐴𝑡𝐵} ≠ ∅)
5352, 24sylibr 234 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝑠𝐴𝑡𝑠 / 𝑥𝐵)) → 𝑡 𝑥𝐴 𝐵)
54 breq2 5170 . . . . . . . . . . 11 (𝑟 = (𝐹𝑡) → (𝑠𝑅𝑟𝑠𝑅(𝐹𝑡)))
5554notbid 318 . . . . . . . . . 10 (𝑟 = (𝐹𝑡) → (¬ 𝑠𝑅𝑟 ↔ ¬ 𝑠𝑅(𝐹𝑡)))
5655ralbidv 3184 . . . . . . . . 9 (𝑟 = (𝐹𝑡) → (∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟 ↔ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅(𝐹𝑡)))
5756elrab 3708 . . . . . . . 8 ((𝐹𝑡) ∈ {𝑟 ∈ {𝑥𝐴𝑡𝐵} ∣ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟} ↔ ((𝐹𝑡) ∈ {𝑥𝐴𝑡𝐵} ∧ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅(𝐹𝑡)))
5857simprbi 496 . . . . . . 7 ((𝐹𝑡) ∈ {𝑟 ∈ {𝑥𝐴𝑡𝐵} ∣ ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅𝑟} → ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅(𝐹𝑡))
5931, 58syl 17 . . . . . 6 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ 𝑡 𝑥𝐴 𝐵) → ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅(𝐹𝑡))
6053, 59syldan 590 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝑠𝐴𝑡𝑠 / 𝑥𝐵)) → ∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅(𝐹𝑡))
61 rsp 3253 . . . . 5 (∀𝑠 ∈ {𝑥𝐴𝑡𝐵} ¬ 𝑠𝑅(𝐹𝑡) → (𝑠 ∈ {𝑥𝐴𝑡𝐵} → ¬ 𝑠𝑅(𝐹𝑡)))
6260, 51, 61sylc 65 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ (𝑠𝐴𝑡𝑠 / 𝑥𝐵)) → ¬ 𝑠𝑅(𝐹𝑡))
6362ralrimivva 3208 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴) → ∀𝑠𝐴𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡))
6437, 46, 633jca 1128 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴) → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑠𝐴𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡)))
651, 2, 64syl2anc 583 1 (𝜑 → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑠𝐴𝑡 𝑠 / 𝑥𝐵 ¬ 𝑠𝑅(𝐹𝑡)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 846  w3a 1087   = wceq 1537  wcel 2108  wne 2946  wral 3067  wrex 3076  ∃!wreu 3386  {crab 3443  [wsbc 3804  csb 3921  wss 3976  c0 4352   ciun 5015   class class class wbr 5166  {copab 5228  cmpt 5249   Se wse 5650   We wwe 5651   Fn wfn 6568  wf 6569  cfv 6573  crio 7403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-riota 7404
This theorem is referenced by:  weiunfrlem  36430  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434
  Copyright terms: Public domain W3C validator