Metamath Proof Explorer


Theorem weiunso

Description: A strict ordering on an indexed union can be constructed from a well-ordering on its index class and a collection of strict orderings on its members. (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Hypotheses weiun.1 𝐹 = ( 𝑤 𝑥𝐴 𝐵 ↦ ( 𝑢 ∈ { 𝑥𝐴𝑤𝐵 } ∀ 𝑣 ∈ { 𝑥𝐴𝑤𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
weiun.2 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝑦 ) 𝑅 ( 𝐹𝑧 ) ∨ ( ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ∧ 𝑦 ( 𝐹𝑦 ) / 𝑥 𝑆 𝑧 ) ) ) }
Assertion weiunso ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) → 𝑇 Or 𝑥𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 weiun.1 𝐹 = ( 𝑤 𝑥𝐴 𝐵 ↦ ( 𝑢 ∈ { 𝑥𝐴𝑤𝐵 } ∀ 𝑣 ∈ { 𝑥𝐴𝑤𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2 weiun.2 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 𝑥𝐴 𝐵𝑧 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝑦 ) 𝑅 ( 𝐹𝑧 ) ∨ ( ( 𝐹𝑦 ) = ( 𝐹𝑧 ) ∧ 𝑦 ( 𝐹𝑦 ) / 𝑥 𝑆 𝑧 ) ) ) }
3 sopo ( 𝑆 Or 𝐵𝑆 Po 𝐵 )
4 3 ralimi ( ∀ 𝑥𝐴 𝑆 Or 𝐵 → ∀ 𝑥𝐴 𝑆 Po 𝐵 )
5 1 2 weiunpo ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Po 𝐵 ) → 𝑇 Po 𝑥𝐴 𝐵 )
6 4 5 syl3an3 ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) → 𝑇 Po 𝑥𝐴 𝐵 )
7 simplrl ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ) → 𝑞 𝑥𝐴 𝐵 )
8 simplrr ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ) → 𝑟 𝑥𝐴 𝐵 )
9 animorrl ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ) → ( ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ∨ ( ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ∧ 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟 ) ) )
10 1 2 weiunlem1 ( 𝑞 𝑇 𝑟 ↔ ( ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ∨ ( ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ∧ 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟 ) ) ) )
11 7 8 9 10 syl21anbrc ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ) → 𝑞 𝑇 𝑟 )
12 11 3mix1d ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ) → ( 𝑞 𝑇 𝑟𝑞 = 𝑟𝑟 𝑇 𝑞 ) )
13 csbeq1 ( 𝑠 = ( 𝐹𝑞 ) → 𝑠 / 𝑥 𝑆 = ( 𝐹𝑞 ) / 𝑥 𝑆 )
14 csbeq1 ( 𝑠 = ( 𝐹𝑞 ) → 𝑠 / 𝑥 𝐵 = ( 𝐹𝑞 ) / 𝑥 𝐵 )
15 13 14 soeq12d ( 𝑠 = ( 𝐹𝑞 ) → ( 𝑠 / 𝑥 𝑆 Or 𝑠 / 𝑥 𝐵 ( 𝐹𝑞 ) / 𝑥 𝑆 Or ( 𝐹𝑞 ) / 𝑥 𝐵 ) )
16 simpll3 ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ∀ 𝑥𝐴 𝑆 Or 𝐵 )
17 nfv 𝑠 𝑆 Or 𝐵
18 nfcsb1v 𝑥 𝑠 / 𝑥 𝑆
19 nfcsb1v 𝑥 𝑠 / 𝑥 𝐵
20 18 19 nfso 𝑥 𝑠 / 𝑥 𝑆 Or 𝑠 / 𝑥 𝐵
21 csbeq1a ( 𝑥 = 𝑠𝑆 = 𝑠 / 𝑥 𝑆 )
22 csbeq1a ( 𝑥 = 𝑠𝐵 = 𝑠 / 𝑥 𝐵 )
23 21 22 soeq12d ( 𝑥 = 𝑠 → ( 𝑆 Or 𝐵 𝑠 / 𝑥 𝑆 Or 𝑠 / 𝑥 𝐵 ) )
24 17 20 23 cbvralw ( ∀ 𝑥𝐴 𝑆 Or 𝐵 ↔ ∀ 𝑠𝐴 𝑠 / 𝑥 𝑆 Or 𝑠 / 𝑥 𝐵 )
25 16 24 sylib ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ∀ 𝑠𝐴 𝑠 / 𝑥 𝑆 Or 𝑠 / 𝑥 𝐵 )
26 simpl1 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → 𝑅 We 𝐴 )
27 simpl2 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → 𝑅 Se 𝐴 )
28 1 2 26 27 weiunlem2 ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → ( 𝐹 : 𝑥𝐴 𝐵𝐴 ∧ ∀ 𝑡 𝑥𝐴 𝐵 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵 ∧ ∀ 𝑠𝐴𝑡 𝑠 / 𝑥 𝐵 ¬ 𝑠 𝑅 ( 𝐹𝑡 ) ) )
29 28 simp1d ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → 𝐹 : 𝑥𝐴 𝐵𝐴 )
30 simprl ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → 𝑞 𝑥𝐴 𝐵 )
31 29 30 ffvelcdmd ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → ( 𝐹𝑞 ) ∈ 𝐴 )
32 31 adantr ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝐹𝑞 ) ∈ 𝐴 )
33 15 25 32 rspcdva ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝐹𝑞 ) / 𝑥 𝑆 Or ( 𝐹𝑞 ) / 𝑥 𝐵 )
34 id ( 𝑡 = 𝑞𝑡 = 𝑞 )
35 fveq2 ( 𝑡 = 𝑞 → ( 𝐹𝑡 ) = ( 𝐹𝑞 ) )
36 35 csbeq1d ( 𝑡 = 𝑞 ( 𝐹𝑡 ) / 𝑥 𝐵 = ( 𝐹𝑞 ) / 𝑥 𝐵 )
37 34 36 eleq12d ( 𝑡 = 𝑞 → ( 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵𝑞 ( 𝐹𝑞 ) / 𝑥 𝐵 ) )
38 28 simp2d ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → ∀ 𝑡 𝑥𝐴 𝐵 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵 )
39 38 adantr ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ∀ 𝑡 𝑥𝐴 𝐵 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵 )
40 simplrl ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → 𝑞 𝑥𝐴 𝐵 )
41 37 39 40 rspcdva ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → 𝑞 ( 𝐹𝑞 ) / 𝑥 𝐵 )
42 id ( 𝑡 = 𝑟𝑡 = 𝑟 )
43 fveq2 ( 𝑡 = 𝑟 → ( 𝐹𝑡 ) = ( 𝐹𝑟 ) )
44 43 csbeq1d ( 𝑡 = 𝑟 ( 𝐹𝑡 ) / 𝑥 𝐵 = ( 𝐹𝑟 ) / 𝑥 𝐵 )
45 42 44 eleq12d ( 𝑡 = 𝑟 → ( 𝑡 ( 𝐹𝑡 ) / 𝑥 𝐵𝑟 ( 𝐹𝑟 ) / 𝑥 𝐵 ) )
46 simplrr ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → 𝑟 𝑥𝐴 𝐵 )
47 45 39 46 rspcdva ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → 𝑟 ( 𝐹𝑟 ) / 𝑥 𝐵 )
48 simpr ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝐹𝑞 ) = ( 𝐹𝑟 ) )
49 48 csbeq1d ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝐹𝑞 ) / 𝑥 𝐵 = ( 𝐹𝑟 ) / 𝑥 𝐵 )
50 47 49 eleqtrrd ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → 𝑟 ( 𝐹𝑞 ) / 𝑥 𝐵 )
51 solin ( ( ( 𝐹𝑞 ) / 𝑥 𝑆 Or ( 𝐹𝑞 ) / 𝑥 𝐵 ∧ ( 𝑞 ( 𝐹𝑞 ) / 𝑥 𝐵𝑟 ( 𝐹𝑞 ) / 𝑥 𝐵 ) ) → ( 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟𝑞 = 𝑟𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) )
52 33 41 50 51 syl12anc ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟𝑞 = 𝑟𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) )
53 simpllr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟 ) → ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) )
54 48 anim1i ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟 ) → ( ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ∧ 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟 ) )
55 54 olcd ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟 ) → ( ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ∨ ( ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ∧ 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟 ) ) )
56 53 55 10 sylanbrc ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟 ) → 𝑞 𝑇 𝑟 )
57 56 ex ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟𝑞 𝑇 𝑟 ) )
58 idd ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝑞 = 𝑟𝑞 = 𝑟 ) )
59 46 adantr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → 𝑟 𝑥𝐴 𝐵 )
60 40 adantr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → 𝑞 𝑥𝐴 𝐵 )
61 simplr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → ( 𝐹𝑞 ) = ( 𝐹𝑟 ) )
62 61 eqcomd ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → ( 𝐹𝑟 ) = ( 𝐹𝑞 ) )
63 61 csbeq1d ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → ( 𝐹𝑞 ) / 𝑥 𝑆 = ( 𝐹𝑟 ) / 𝑥 𝑆 )
64 simpr ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 )
65 63 64 breqdi ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → 𝑟 ( 𝐹𝑟 ) / 𝑥 𝑆 𝑞 )
66 62 65 jca ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → ( ( 𝐹𝑟 ) = ( 𝐹𝑞 ) ∧ 𝑟 ( 𝐹𝑟 ) / 𝑥 𝑆 𝑞 ) )
67 66 olcd ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → ( ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ∨ ( ( 𝐹𝑟 ) = ( 𝐹𝑞 ) ∧ 𝑟 ( 𝐹𝑟 ) / 𝑥 𝑆 𝑞 ) ) )
68 1 2 weiunlem1 ( 𝑟 𝑇 𝑞 ↔ ( ( 𝑟 𝑥𝐴 𝐵𝑞 𝑥𝐴 𝐵 ) ∧ ( ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ∨ ( ( 𝐹𝑟 ) = ( 𝐹𝑞 ) ∧ 𝑟 ( 𝐹𝑟 ) / 𝑥 𝑆 𝑞 ) ) ) )
69 59 60 67 68 syl21anbrc ( ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) ∧ 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → 𝑟 𝑇 𝑞 )
70 69 ex ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞𝑟 𝑇 𝑞 ) )
71 57 58 70 3orim123d ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( ( 𝑞 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑟𝑞 = 𝑟𝑟 ( 𝐹𝑞 ) / 𝑥 𝑆 𝑞 ) → ( 𝑞 𝑇 𝑟𝑞 = 𝑟𝑟 𝑇 𝑞 ) ) )
72 52 71 mpd ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ) → ( 𝑞 𝑇 𝑟𝑞 = 𝑟𝑟 𝑇 𝑞 ) )
73 simplrr ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ) → 𝑟 𝑥𝐴 𝐵 )
74 simplrl ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ) → 𝑞 𝑥𝐴 𝐵 )
75 animorrl ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ) → ( ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ∨ ( ( 𝐹𝑟 ) = ( 𝐹𝑞 ) ∧ 𝑟 ( 𝐹𝑟 ) / 𝑥 𝑆 𝑞 ) ) )
76 73 74 75 68 syl21anbrc ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ) → 𝑟 𝑇 𝑞 )
77 76 3mix3d ( ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) ∧ ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ) → ( 𝑞 𝑇 𝑟𝑞 = 𝑟𝑟 𝑇 𝑞 ) )
78 weso ( 𝑅 We 𝐴𝑅 Or 𝐴 )
79 26 78 syl ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → 𝑅 Or 𝐴 )
80 simprr ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → 𝑟 𝑥𝐴 𝐵 )
81 29 80 ffvelcdmd ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → ( 𝐹𝑟 ) ∈ 𝐴 )
82 solin ( ( 𝑅 Or 𝐴 ∧ ( ( 𝐹𝑞 ) ∈ 𝐴 ∧ ( 𝐹𝑟 ) ∈ 𝐴 ) ) → ( ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ∨ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ∨ ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ) )
83 79 31 81 82 syl12anc ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → ( ( 𝐹𝑞 ) 𝑅 ( 𝐹𝑟 ) ∨ ( 𝐹𝑞 ) = ( 𝐹𝑟 ) ∨ ( 𝐹𝑟 ) 𝑅 ( 𝐹𝑞 ) ) )
84 12 72 77 83 mpjao3dan ( ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 𝑥𝐴 𝐵𝑟 𝑥𝐴 𝐵 ) ) → ( 𝑞 𝑇 𝑟𝑞 = 𝑟𝑟 𝑇 𝑞 ) )
85 6 84 issod ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ∧ ∀ 𝑥𝐴 𝑆 Or 𝐵 ) → 𝑇 Or 𝑥𝐴 𝐵 )