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

Theorem weiunso 36379
Description: A strict ordering on an indexed union can be constructed from a well-ordering on its index set and a collection of strict orderings on its members. (Contributed by Matthew House, 23-Aug-2025.)
Hypotheses
Ref Expression
weiunso.1 𝐹 = (𝑤 𝑥𝐴 𝐵 ↦ (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢))
weiunso.2 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵) ∧ ((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)))}
Assertion
Ref Expression
weiunso ((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) → 𝑇 Or 𝑥𝐴 𝐵)
Distinct variable groups:   𝑢,𝐴,𝑣,𝑤,𝑥   𝑦,𝐴,𝑧,𝑥   𝑢,𝐵,𝑣,𝑤   𝑦,𝐵,𝑧   𝑦,𝐹,𝑧   𝑢,𝑅,𝑣,𝑤   𝑦,𝑅,𝑧   𝑦,𝑆,𝑧
Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥,𝑤,𝑣,𝑢)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝐹(𝑥,𝑤,𝑣,𝑢)

Proof of Theorem weiunso
Dummy variables 𝑞 𝑠 𝑡 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sopo 5630 . . . 4 (𝑆 Or 𝐵𝑆 Po 𝐵)
21ralimi 3085 . . 3 (∀𝑥𝐴 𝑆 Or 𝐵 → ∀𝑥𝐴 𝑆 Po 𝐵)
3 weiunso.1 . . . 4 𝐹 = (𝑤 𝑥𝐴 𝐵 ↦ (𝑢 ∈ {𝑥𝐴𝑤𝐵}∀𝑣 ∈ {𝑥𝐴𝑤𝐵} ¬ 𝑣𝑅𝑢))
4 weiunso.2 . . . 4 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵) ∧ ((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)))}
53, 4weiunpo 36378 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Po 𝐵) → 𝑇 Po 𝑥𝐴 𝐵)
62, 5syl3an3 1165 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) → 𝑇 Po 𝑥𝐴 𝐵)
7 simplrl 776 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞)𝑅(𝐹𝑟)) → 𝑞 𝑥𝐴 𝐵)
8 simplrr 777 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞)𝑅(𝐹𝑟)) → 𝑟 𝑥𝐴 𝐵)
9 animorrl 981 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞)𝑅(𝐹𝑟)) → ((𝐹𝑞)𝑅(𝐹𝑟) ∨ ((𝐹𝑞) = (𝐹𝑟) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟)))
10 simpl 482 . . . . . . . . 9 ((𝑦 = 𝑞𝑧 = 𝑟) → 𝑦 = 𝑞)
1110fveq2d 6923 . . . . . . . 8 ((𝑦 = 𝑞𝑧 = 𝑟) → (𝐹𝑦) = (𝐹𝑞))
12 simpr 484 . . . . . . . . 9 ((𝑦 = 𝑞𝑧 = 𝑟) → 𝑧 = 𝑟)
1312fveq2d 6923 . . . . . . . 8 ((𝑦 = 𝑞𝑧 = 𝑟) → (𝐹𝑧) = (𝐹𝑟))
1411, 13breq12d 5182 . . . . . . 7 ((𝑦 = 𝑞𝑧 = 𝑟) → ((𝐹𝑦)𝑅(𝐹𝑧) ↔ (𝐹𝑞)𝑅(𝐹𝑟)))
1511, 13eqeq12d 2750 . . . . . . . 8 ((𝑦 = 𝑞𝑧 = 𝑟) → ((𝐹𝑦) = (𝐹𝑧) ↔ (𝐹𝑞) = (𝐹𝑟)))
1611csbeq1d 3919 . . . . . . . . 9 ((𝑦 = 𝑞𝑧 = 𝑟) → (𝐹𝑦) / 𝑥𝑆 = (𝐹𝑞) / 𝑥𝑆)
1710, 16, 12breq123d 5183 . . . . . . . 8 ((𝑦 = 𝑞𝑧 = 𝑟) → (𝑦(𝐹𝑦) / 𝑥𝑆𝑧𝑞(𝐹𝑞) / 𝑥𝑆𝑟))
1815, 17anbi12d 631 . . . . . . 7 ((𝑦 = 𝑞𝑧 = 𝑟) → (((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧) ↔ ((𝐹𝑞) = (𝐹𝑟) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟)))
1914, 18orbi12d 917 . . . . . 6 ((𝑦 = 𝑞𝑧 = 𝑟) → (((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)) ↔ ((𝐹𝑞)𝑅(𝐹𝑟) ∨ ((𝐹𝑞) = (𝐹𝑟) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟))))
2019, 4brab2a 5792 . . . . 5 (𝑞𝑇𝑟 ↔ ((𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵) ∧ ((𝐹𝑞)𝑅(𝐹𝑟) ∨ ((𝐹𝑞) = (𝐹𝑟) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟))))
217, 8, 9, 20syl21anbrc 1344 . . . 4 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞)𝑅(𝐹𝑟)) → 𝑞𝑇𝑟)
22213mix1d 1336 . . 3 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞)𝑅(𝐹𝑟)) → (𝑞𝑇𝑟𝑞 = 𝑟𝑟𝑇𝑞))
23 csbeq1 3918 . . . . . . . 8 (𝑠 = (𝐹𝑞) → 𝑠 / 𝑥𝑆 = (𝐹𝑞) / 𝑥𝑆)
24 soeq1 5632 . . . . . . . 8 (𝑠 / 𝑥𝑆 = (𝐹𝑞) / 𝑥𝑆 → (𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵(𝐹𝑞) / 𝑥𝑆 Or 𝑠 / 𝑥𝐵))
2523, 24syl 17 . . . . . . 7 (𝑠 = (𝐹𝑞) → (𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵(𝐹𝑞) / 𝑥𝑆 Or 𝑠 / 𝑥𝐵))
26 csbeq1 3918 . . . . . . . 8 (𝑠 = (𝐹𝑞) → 𝑠 / 𝑥𝐵 = (𝐹𝑞) / 𝑥𝐵)
27 soeq2 5633 . . . . . . . 8 (𝑠 / 𝑥𝐵 = (𝐹𝑞) / 𝑥𝐵 → ((𝐹𝑞) / 𝑥𝑆 Or 𝑠 / 𝑥𝐵(𝐹𝑞) / 𝑥𝑆 Or (𝐹𝑞) / 𝑥𝐵))
2826, 27syl 17 . . . . . . 7 (𝑠 = (𝐹𝑞) → ((𝐹𝑞) / 𝑥𝑆 Or 𝑠 / 𝑥𝐵(𝐹𝑞) / 𝑥𝑆 Or (𝐹𝑞) / 𝑥𝐵))
2925, 28bitrd 279 . . . . . 6 (𝑠 = (𝐹𝑞) → (𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵(𝐹𝑞) / 𝑥𝑆 Or (𝐹𝑞) / 𝑥𝐵))
30 simpll3 1214 . . . . . . 7 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → ∀𝑥𝐴 𝑆 Or 𝐵)
31 nfv 1913 . . . . . . . 8 𝑠 𝑆 Or 𝐵
32 nfcsb1v 3940 . . . . . . . . 9 𝑥𝑠 / 𝑥𝑆
33 nfcsb1v 3940 . . . . . . . . 9 𝑥𝑠 / 𝑥𝐵
3432, 33nfso 5617 . . . . . . . 8 𝑥𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵
35 csbeq1a 3929 . . . . . . . . . 10 (𝑥 = 𝑠𝑆 = 𝑠 / 𝑥𝑆)
36 soeq1 5632 . . . . . . . . . 10 (𝑆 = 𝑠 / 𝑥𝑆 → (𝑆 Or 𝐵𝑠 / 𝑥𝑆 Or 𝐵))
3735, 36syl 17 . . . . . . . . 9 (𝑥 = 𝑠 → (𝑆 Or 𝐵𝑠 / 𝑥𝑆 Or 𝐵))
38 csbeq1a 3929 . . . . . . . . . 10 (𝑥 = 𝑠𝐵 = 𝑠 / 𝑥𝐵)
39 soeq2 5633 . . . . . . . . . 10 (𝐵 = 𝑠 / 𝑥𝐵 → (𝑠 / 𝑥𝑆 Or 𝐵𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵))
4038, 39syl 17 . . . . . . . . 9 (𝑥 = 𝑠 → (𝑠 / 𝑥𝑆 Or 𝐵𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵))
4137, 40bitrd 279 . . . . . . . 8 (𝑥 = 𝑠 → (𝑆 Or 𝐵𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵))
4231, 34, 41cbvralw 3307 . . . . . . 7 (∀𝑥𝐴 𝑆 Or 𝐵 ↔ ∀𝑠𝐴 𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵)
4330, 42sylib 218 . . . . . 6 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → ∀𝑠𝐴 𝑠 / 𝑥𝑆 Or 𝑠 / 𝑥𝐵)
44 simpl1 1191 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → 𝑅 We 𝐴)
45 simpl2 1192 . . . . . . . . . 10 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → 𝑅 Se 𝐴)
463weiunlem2 36377 . . . . . . . . . 10 ((𝑅 We 𝐴𝑅 Se 𝐴) → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑡 𝑥𝐴 𝐵𝑠𝐴 (𝑡𝑠 / 𝑥𝐵 → ¬ 𝑠𝑅(𝐹𝑡))))
4744, 45, 46syl2anc 583 . . . . . . . . 9 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → (𝐹: 𝑥𝐴 𝐵𝐴 ∧ ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵 ∧ ∀𝑡 𝑥𝐴 𝐵𝑠𝐴 (𝑡𝑠 / 𝑥𝐵 → ¬ 𝑠𝑅(𝐹𝑡))))
4847simp1d 1142 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → 𝐹: 𝑥𝐴 𝐵𝐴)
49 simprl 770 . . . . . . . 8 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → 𝑞 𝑥𝐴 𝐵)
5048, 49ffvelcdmd 7117 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → (𝐹𝑞) ∈ 𝐴)
5150adantr 480 . . . . . 6 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝐹𝑞) ∈ 𝐴)
5229, 43, 51rspcdva 3632 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝐹𝑞) / 𝑥𝑆 Or (𝐹𝑞) / 𝑥𝐵)
53 id 22 . . . . . . 7 (𝑡 = 𝑞𝑡 = 𝑞)
54 fveq2 6919 . . . . . . . 8 (𝑡 = 𝑞 → (𝐹𝑡) = (𝐹𝑞))
5554csbeq1d 3919 . . . . . . 7 (𝑡 = 𝑞(𝐹𝑡) / 𝑥𝐵 = (𝐹𝑞) / 𝑥𝐵)
5653, 55eleq12d 2832 . . . . . 6 (𝑡 = 𝑞 → (𝑡(𝐹𝑡) / 𝑥𝐵𝑞(𝐹𝑞) / 𝑥𝐵))
5747simp2d 1143 . . . . . . 7 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵)
5857adantr 480 . . . . . 6 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → ∀𝑡 𝑥𝐴 𝐵𝑡(𝐹𝑡) / 𝑥𝐵)
59 simplrl 776 . . . . . 6 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → 𝑞 𝑥𝐴 𝐵)
6056, 58, 59rspcdva 3632 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → 𝑞(𝐹𝑞) / 𝑥𝐵)
61 id 22 . . . . . . . 8 (𝑡 = 𝑟𝑡 = 𝑟)
62 fveq2 6919 . . . . . . . . 9 (𝑡 = 𝑟 → (𝐹𝑡) = (𝐹𝑟))
6362csbeq1d 3919 . . . . . . . 8 (𝑡 = 𝑟(𝐹𝑡) / 𝑥𝐵 = (𝐹𝑟) / 𝑥𝐵)
6461, 63eleq12d 2832 . . . . . . 7 (𝑡 = 𝑟 → (𝑡(𝐹𝑡) / 𝑥𝐵𝑟(𝐹𝑟) / 𝑥𝐵))
65 simplrr 777 . . . . . . 7 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → 𝑟 𝑥𝐴 𝐵)
6664, 58, 65rspcdva 3632 . . . . . 6 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → 𝑟(𝐹𝑟) / 𝑥𝐵)
67 simpr 484 . . . . . . 7 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝐹𝑞) = (𝐹𝑟))
6867csbeq1d 3919 . . . . . 6 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝐹𝑞) / 𝑥𝐵 = (𝐹𝑟) / 𝑥𝐵)
6966, 68eleqtrrd 2841 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → 𝑟(𝐹𝑞) / 𝑥𝐵)
70 solin 5636 . . . . 5 (((𝐹𝑞) / 𝑥𝑆 Or (𝐹𝑞) / 𝑥𝐵 ∧ (𝑞(𝐹𝑞) / 𝑥𝐵𝑟(𝐹𝑞) / 𝑥𝐵)) → (𝑞(𝐹𝑞) / 𝑥𝑆𝑟𝑞 = 𝑟𝑟(𝐹𝑞) / 𝑥𝑆𝑞))
7152, 60, 69, 70syl12anc 836 . . . 4 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝑞(𝐹𝑞) / 𝑥𝑆𝑟𝑞 = 𝑟𝑟(𝐹𝑞) / 𝑥𝑆𝑞))
72 simpllr 775 . . . . . . 7 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟) → (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵))
7367anim1i 614 . . . . . . . 8 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟) → ((𝐹𝑞) = (𝐹𝑟) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟))
7473olcd 873 . . . . . . 7 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟) → ((𝐹𝑞)𝑅(𝐹𝑟) ∨ ((𝐹𝑞) = (𝐹𝑟) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟)))
7572, 74, 20sylanbrc 582 . . . . . 6 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑞(𝐹𝑞) / 𝑥𝑆𝑟) → 𝑞𝑇𝑟)
7675ex 412 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝑞(𝐹𝑞) / 𝑥𝑆𝑟𝑞𝑇𝑟))
77 idd 24 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝑞 = 𝑟𝑞 = 𝑟))
7865adantr 480 . . . . . . 7 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → 𝑟 𝑥𝐴 𝐵)
7959adantr 480 . . . . . . 7 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → 𝑞 𝑥𝐴 𝐵)
80 simplr 768 . . . . . . . . . 10 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → (𝐹𝑞) = (𝐹𝑟))
8180eqcomd 2740 . . . . . . . . 9 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → (𝐹𝑟) = (𝐹𝑞))
8280csbeq1d 3919 . . . . . . . . . 10 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → (𝐹𝑞) / 𝑥𝑆 = (𝐹𝑟) / 𝑥𝑆)
83 simpr 484 . . . . . . . . . 10 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → 𝑟(𝐹𝑞) / 𝑥𝑆𝑞)
8482, 83breqdi 5184 . . . . . . . . 9 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → 𝑟(𝐹𝑟) / 𝑥𝑆𝑞)
8581, 84jca 511 . . . . . . . 8 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → ((𝐹𝑟) = (𝐹𝑞) ∧ 𝑟(𝐹𝑟) / 𝑥𝑆𝑞))
8685olcd 873 . . . . . . 7 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → ((𝐹𝑟)𝑅(𝐹𝑞) ∨ ((𝐹𝑟) = (𝐹𝑞) ∧ 𝑟(𝐹𝑟) / 𝑥𝑆𝑞)))
87 simpl 482 . . . . . . . . . . 11 ((𝑦 = 𝑟𝑧 = 𝑞) → 𝑦 = 𝑟)
8887fveq2d 6923 . . . . . . . . . 10 ((𝑦 = 𝑟𝑧 = 𝑞) → (𝐹𝑦) = (𝐹𝑟))
89 simpr 484 . . . . . . . . . . 11 ((𝑦 = 𝑟𝑧 = 𝑞) → 𝑧 = 𝑞)
9089fveq2d 6923 . . . . . . . . . 10 ((𝑦 = 𝑟𝑧 = 𝑞) → (𝐹𝑧) = (𝐹𝑞))
9188, 90breq12d 5182 . . . . . . . . 9 ((𝑦 = 𝑟𝑧 = 𝑞) → ((𝐹𝑦)𝑅(𝐹𝑧) ↔ (𝐹𝑟)𝑅(𝐹𝑞)))
9288, 90eqeq12d 2750 . . . . . . . . . 10 ((𝑦 = 𝑟𝑧 = 𝑞) → ((𝐹𝑦) = (𝐹𝑧) ↔ (𝐹𝑟) = (𝐹𝑞)))
9388csbeq1d 3919 . . . . . . . . . . 11 ((𝑦 = 𝑟𝑧 = 𝑞) → (𝐹𝑦) / 𝑥𝑆 = (𝐹𝑟) / 𝑥𝑆)
9487, 93, 89breq123d 5183 . . . . . . . . . 10 ((𝑦 = 𝑟𝑧 = 𝑞) → (𝑦(𝐹𝑦) / 𝑥𝑆𝑧𝑟(𝐹𝑟) / 𝑥𝑆𝑞))
9592, 94anbi12d 631 . . . . . . . . 9 ((𝑦 = 𝑟𝑧 = 𝑞) → (((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧) ↔ ((𝐹𝑟) = (𝐹𝑞) ∧ 𝑟(𝐹𝑟) / 𝑥𝑆𝑞)))
9691, 95orbi12d 917 . . . . . . . 8 ((𝑦 = 𝑟𝑧 = 𝑞) → (((𝐹𝑦)𝑅(𝐹𝑧) ∨ ((𝐹𝑦) = (𝐹𝑧) ∧ 𝑦(𝐹𝑦) / 𝑥𝑆𝑧)) ↔ ((𝐹𝑟)𝑅(𝐹𝑞) ∨ ((𝐹𝑟) = (𝐹𝑞) ∧ 𝑟(𝐹𝑟) / 𝑥𝑆𝑞))))
9796, 4brab2a 5792 . . . . . . 7 (𝑟𝑇𝑞 ↔ ((𝑟 𝑥𝐴 𝐵𝑞 𝑥𝐴 𝐵) ∧ ((𝐹𝑟)𝑅(𝐹𝑞) ∨ ((𝐹𝑟) = (𝐹𝑞) ∧ 𝑟(𝐹𝑟) / 𝑥𝑆𝑞))))
9878, 79, 86, 97syl21anbrc 1344 . . . . . 6 (((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) ∧ 𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → 𝑟𝑇𝑞)
9998ex 412 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝑟(𝐹𝑞) / 𝑥𝑆𝑞𝑟𝑇𝑞))
10076, 77, 993orim123d 1444 . . . 4 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → ((𝑞(𝐹𝑞) / 𝑥𝑆𝑟𝑞 = 𝑟𝑟(𝐹𝑞) / 𝑥𝑆𝑞) → (𝑞𝑇𝑟𝑞 = 𝑟𝑟𝑇𝑞)))
10171, 100mpd 15 . . 3 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑞) = (𝐹𝑟)) → (𝑞𝑇𝑟𝑞 = 𝑟𝑟𝑇𝑞))
102 simplrr 777 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑟)𝑅(𝐹𝑞)) → 𝑟 𝑥𝐴 𝐵)
103 simplrl 776 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑟)𝑅(𝐹𝑞)) → 𝑞 𝑥𝐴 𝐵)
104 animorrl 981 . . . . 5 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑟)𝑅(𝐹𝑞)) → ((𝐹𝑟)𝑅(𝐹𝑞) ∨ ((𝐹𝑟) = (𝐹𝑞) ∧ 𝑟(𝐹𝑟) / 𝑥𝑆𝑞)))
105102, 103, 104, 97syl21anbrc 1344 . . . 4 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑟)𝑅(𝐹𝑞)) → 𝑟𝑇𝑞)
1061053mix3d 1338 . . 3 ((((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) ∧ (𝐹𝑟)𝑅(𝐹𝑞)) → (𝑞𝑇𝑟𝑞 = 𝑟𝑟𝑇𝑞))
107 weso 5690 . . . . 5 (𝑅 We 𝐴𝑅 Or 𝐴)
10844, 107syl 17 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → 𝑅 Or 𝐴)
109 simprr 772 . . . . 5 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → 𝑟 𝑥𝐴 𝐵)
11048, 109ffvelcdmd 7117 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → (𝐹𝑟) ∈ 𝐴)
111 solin 5636 . . . 4 ((𝑅 Or 𝐴 ∧ ((𝐹𝑞) ∈ 𝐴 ∧ (𝐹𝑟) ∈ 𝐴)) → ((𝐹𝑞)𝑅(𝐹𝑟) ∨ (𝐹𝑞) = (𝐹𝑟) ∨ (𝐹𝑟)𝑅(𝐹𝑞)))
112108, 50, 110, 111syl12anc 836 . . 3 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → ((𝐹𝑞)𝑅(𝐹𝑟) ∨ (𝐹𝑞) = (𝐹𝑟) ∨ (𝐹𝑟)𝑅(𝐹𝑞)))
11322, 101, 106, 112mpjao3dan 1432 . 2 (((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) ∧ (𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵)) → (𝑞𝑇𝑟𝑞 = 𝑟𝑟𝑇𝑞))
1146, 113issod 5644 1 ((𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀𝑥𝐴 𝑆 Or 𝐵) → 𝑇 Or 𝑥𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 846  w3o 1086  w3a 1087   = wceq 1537  wcel 2103  wral 3063  {crab 3438  csb 3915   ciun 5019   class class class wbr 5169  {copab 5231  cmpt 5252   Po wpo 5609   Or wor 5610   Se wse 5652   We wwe 5653  wf 6568  cfv 6572  crio 7400
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 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pr 5450
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 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-po 5611  df-so 5612  df-fr 5654  df-se 5655  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-fv 6580  df-riota 7401
This theorem is referenced by:  weiunwe  36384
  Copyright terms: Public domain W3C validator