Metamath Proof Explorer

Theorem weiunso

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)

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

Proof

Step Hyp Ref Expression
1 weiunso.1 ⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2 weiunso.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 simpl ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → 𝑦 = 𝑞 )
11 10 fveq2d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑞 ) )
12 simpr ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → 𝑧 = 𝑟 )
13 12 fveq2d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑟 ) )
14 11 13 breq12d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) )
15 11 13 eqeq12d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) )
16 11 csbeq1d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 )
17 10 16 12 breq123d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
18 15 17 anbi12d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
19 14 18 orbi12d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
20 19 2 brab2a ⊢ ( 𝑞 𝑇 𝑟 ↔ ( ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
21 7 8 9 20 syl21anbrc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → 𝑞 𝑇 𝑟 )
22 21 3mix1d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( 𝑞 𝑇 𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟 𝑇 𝑞 ) )
23 csbeq1 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑞 ) → ⦋ 𝑠 / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 )
24 soeq1 ⊢ ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
25 23 24 syl ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑞 ) → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
26 csbeq1 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑞 ) → ⦋ 𝑠 / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
27 soeq2 ⊢ ( ⦋ 𝑠 / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 → ( ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) )
28 26 27 syl ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑞 ) → ( ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) )
29 25 28 bitrd ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑞 ) → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) )
30 simpll3 ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 )
31 nfv ⊢ Ⅎ 𝑠 𝑆 Or 𝐵
32 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝑆
33 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐵
34 32 33 nfso ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵
35 csbeq1a ⊢ ( 𝑥 = 𝑠 → 𝑆 = ⦋ 𝑠 / 𝑥 ⦌ 𝑆 )
36 soeq1 ⊢ ( 𝑆 = ⦋ 𝑠 / 𝑥 ⦌ 𝑆 → ( 𝑆 Or 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or 𝐵 ) )
37 35 36 syl ⊢ ( 𝑥 = 𝑠 → ( 𝑆 Or 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or 𝐵 ) )
38 csbeq1a ⊢ ( 𝑥 = 𝑠 → 𝐵 = ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
39 soeq2 ⊢ ( 𝐵 = ⦋ 𝑠 / 𝑥 ⦌ 𝐵 → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
40 38 39 syl ⊢ ( 𝑥 = 𝑠 → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
41 37 40 bitrd ⊢ ( 𝑥 = 𝑠 → ( 𝑆 Or 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
42 31 34 41 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ↔ ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
43 30 42 sylib ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Or ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
44 simpl1 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑅 We 𝐴 )
45 simpl2 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑅 Se 𝐴 )
46 1 weiunlem2 ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ 𝐴 ( 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 → ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) ) )
47 44 45 46 syl2anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ 𝐴 ( 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 → ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) ) )
48 47 simp1d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
49 simprl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
50 48 49 ffvelcdmd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
51 50 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
52 29 43 51 rspcdva ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
53 id ⊢ ( 𝑡 = 𝑞 → 𝑡 = 𝑞 )
54 fveq2 ⊢ ( 𝑡 = 𝑞 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑞 ) )
55 54 csbeq1d ⊢ ( 𝑡 = 𝑞 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
56 53 55 eleq12d ⊢ ( 𝑡 = 𝑞 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) )
57 47 simp2d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
58 57 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
59 simplrl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
60 56 58 59 rspcdva ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
61 id ⊢ ( 𝑡 = 𝑟 → 𝑡 = 𝑟 )
62 fveq2 ⊢ ( 𝑡 = 𝑟 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑟 ) )
63 62 csbeq1d ⊢ ( 𝑡 = 𝑟 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
64 61 63 eleq12d ⊢ ( 𝑡 = 𝑟 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 ) )
65 simplrr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
66 64 58 65 rspcdva ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
67 simpr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) )
68 67 csbeq1d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
69 66 68 eleqtrrd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
70 solin ⊢ ( ( ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 Or ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ∧ ( 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ∧ 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) ) → ( 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) )
71 52 60 69 70 syl12anc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ( 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) )
72 simpllr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) → ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
73 67 anim1i ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) → ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
74 73 olcd ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
75 72 74 20 sylanbrc ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) → 𝑞 𝑇 𝑟 )
76 75 ex ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ( 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 → 𝑞 𝑇 𝑟 ) )
77 idd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ( 𝑞 = 𝑟 → 𝑞 = 𝑟 ) )
78 65 adantr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
79 59 adantr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
80 simplr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) )
81 80 eqcomd ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) )
82 80 csbeq1d ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 )
83 simpr ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 )
84 82 83 breqdi ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 )
85 81 84 jca ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → ( ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 ) )
86 85 olcd ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → ( ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) )
87 simpl ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → 𝑦 = 𝑟 )
88 87 fveq2d ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑟 ) )
89 simpr ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → 𝑧 = 𝑞 )
90 89 fveq2d ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑞 ) )
91 88 90 breq12d ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) )
92 88 90 eqeq12d ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) ) )
93 88 csbeq1d ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 )
94 87 93 89 breq123d ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 ) )
95 92 94 anbi12d ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) )
96 91 95 orbi12d ⊢ ( ( 𝑦 = 𝑟 ∧ 𝑧 = 𝑞 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) ) )
97 96 2 brab2a ⊢ ( 𝑟 𝑇 𝑞 ↔ ( ( 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) ) )
98 78 79 86 97 syl21anbrc ⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → 𝑟 𝑇 𝑞 )
99 98 ex ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ( 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 → 𝑟 𝑇 𝑞 ) )
100 76 77 99 3orim123d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ( ( 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑞 ) → ( 𝑞 𝑇 𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟 𝑇 𝑞 ) ) )
101 71 100 mpd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) → ( 𝑞 𝑇 𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟 𝑇 𝑞 ) )
102 simplrr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) → 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
103 simplrl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) → 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
104 animorrl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) → ( ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) )
105 102 103 104 97 syl21anbrc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) → 𝑟 𝑇 𝑞 )
106 105 3mix3d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) → ( 𝑞 𝑇 𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟 𝑇 𝑞 ) )
107 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
108 44 107 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑅 Or 𝐴 )
109 simprr ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
110 48 109 ffvelcdmd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 )
111 solin ⊢ ( ( 𝑅 Or 𝐴 ∧ ( ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∨ ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) )
112 108 50 110 111 syl12anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∨ ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) )
113 22 101 106 112 mpjao3dan ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) ∧ ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑞 𝑇 𝑟 ∨ 𝑞 = 𝑟 ∨ 𝑟 𝑇 𝑞 ) )
114 6 113 issod ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Or 𝐵 ) → 𝑇 Or ∪ 𝑥 ∈ 𝐴 𝐵 )