Metamath Proof Explorer

Theorem weiunpo

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

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

Proof

Step Hyp Ref Expression
1 weiunpo.1 ⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2 weiunpo.2 ⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
3 simpl1 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑅 We 𝐴 )
4 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
5 3 4 syl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑅 Or 𝐴 )
6 simpl2 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑅 Se 𝐴 )
7 1 weiunlem2 ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ 𝐴 ( 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 → ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) ) )
8 3 6 7 syl2anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑠 ∈ 𝐴 ( 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 → ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) ) )
9 8 simp1d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
10 simpr1 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
11 9 10 ffvelcdmd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 )
12 sonr ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) )
13 5 11 12 syl2anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) )
14 csbeq1 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑝 ) → ⦋ 𝑠 / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 )
15 poeq1 ⊢ ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
16 14 15 syl ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑝 ) → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
17 csbeq1 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑝 ) → ⦋ 𝑠 / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
18 poeq2 ⊢ ( ⦋ 𝑠 / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 → ( ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) )
19 17 18 syl ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑝 ) → ( ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) )
20 16 19 bitrd ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑝 ) → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) )
21 simpl3 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 )
22 nfv ⊢ Ⅎ 𝑠 𝑆 Po 𝐵
23 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝑆
24 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐵
25 23 24 nfpo ⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵
26 csbeq1a ⊢ ( 𝑥 = 𝑠 → 𝑆 = ⦋ 𝑠 / 𝑥 ⦌ 𝑆 )
27 poeq1 ⊢ ( 𝑆 = ⦋ 𝑠 / 𝑥 ⦌ 𝑆 → ( 𝑆 Po 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po 𝐵 ) )
28 26 27 syl ⊢ ( 𝑥 = 𝑠 → ( 𝑆 Po 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po 𝐵 ) )
29 csbeq1a ⊢ ( 𝑥 = 𝑠 → 𝐵 = ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
30 poeq2 ⊢ ( 𝐵 = ⦋ 𝑠 / 𝑥 ⦌ 𝐵 → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
31 29 30 syl ⊢ ( 𝑥 = 𝑠 → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
32 28 31 bitrd ⊢ ( 𝑥 = 𝑠 → ( 𝑆 Po 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
33 22 25 32 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ↔ ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
34 21 33 sylib ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
35 20 34 11 rspcdva ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
36 id ⊢ ( 𝑡 = 𝑝 → 𝑡 = 𝑝 )
37 fveq2 ⊢ ( 𝑡 = 𝑝 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) )
38 37 csbeq1d ⊢ ( 𝑡 = 𝑝 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
39 36 38 eleq12d ⊢ ( 𝑡 = 𝑝 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) )
40 8 simp2d ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
41 39 40 10 rspcdva ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
42 poirr ⊢ ( ( ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ∧ 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) → ¬ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 )
43 35 41 42 syl2anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 )
44 43 intnand ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) )
45 ioran ⊢ ( ¬ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ↔ ( ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∧ ¬ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
46 13 44 45 sylanbrc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
47 simpl ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → 𝑦 = 𝑝 )
48 47 fveq2d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑝 ) )
49 simpr ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → 𝑧 = 𝑝 )
50 49 fveq2d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑝 ) )
51 48 50 breq12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) )
52 48 50 eqeq12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ) )
53 48 csbeq1d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 )
54 47 53 49 breq123d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) )
55 52 54 anbi12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
56 51 55 orbi12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑝 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) )
57 56 2 brab2a ⊢ ( 𝑝 𝑇 𝑝 ↔ ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) )
58 57 simprbi ⊢ ( 𝑝 𝑇 𝑝 → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
59 46 58 nsyl ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ 𝑝 𝑇 𝑝 )
60 simpr3 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
61 10 60 jca ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
62 simpl ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → 𝑦 = 𝑝 )
63 62 fveq2d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑝 ) )
64 simpr ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → 𝑧 = 𝑞 )
65 64 fveq2d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑞 ) )
66 63 65 breq12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) )
67 63 65 eqeq12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ) )
68 63 csbeq1d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 )
69 62 68 64 breq123d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) )
70 67 69 anbi12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) )
71 66 70 orbi12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑞 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) ) )
72 71 2 brab2a ⊢ ( 𝑝 𝑇 𝑞 ↔ ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) ) )
73 72 simprbi ⊢ ( 𝑝 𝑇 𝑞 → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) )
74 simpl ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → 𝑦 = 𝑞 )
75 74 fveq2d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑞 ) )
76 simpr ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → 𝑧 = 𝑟 )
77 76 fveq2d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑟 ) )
78 75 77 breq12d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) )
79 75 77 eqeq12d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ) )
80 75 csbeq1d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 )
81 74 80 76 breq123d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
82 79 81 anbi12d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
83 78 82 orbi12d ⊢ ( ( 𝑦 = 𝑞 ∧ 𝑧 = 𝑟 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
84 83 2 brab2a ⊢ ( 𝑞 𝑇 𝑟 ↔ ( ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
85 84 simprbi ⊢ ( 𝑞 𝑇 𝑟 → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
86 simpr2 ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
87 9 86 ffvelcdmd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
88 9 60 ffvelcdmd ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 )
89 sotr ⊢ ( ( 𝑅 Or 𝐴 ∧ ( ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) )
90 5 11 87 88 89 syl13anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) )
91 90 imp ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) )
92 91 orcd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
93 92 ex ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
94 simprll ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) )
95 simprr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) )
96 94 95 eqbrtrd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) )
97 96 orcd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
98 97 ex ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
99 simprl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) )
100 simprrl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) )
101 99 100 breqtrd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) )
102 101 orcd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
103 102 ex ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
104 simprll ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) )
105 simprrl ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) )
106 104 105 eqtrd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) )
107 simprlr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 )
108 simprrr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 )
109 104 csbeq1d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 )
110 109 breqd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝑞 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ↔ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
111 108 110 mpbird ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑞 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 )
112 35 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
113 41 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
114 id ⊢ ( 𝑡 = 𝑞 → 𝑡 = 𝑞 )
115 fveq2 ⊢ ( 𝑡 = 𝑞 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑞 ) )
116 115 csbeq1d ⊢ ( 𝑡 = 𝑞 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
117 114 116 eleq12d ⊢ ( 𝑡 = 𝑞 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) )
118 117 40 86 rspcdva ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
119 118 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
120 104 csbeq1d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
121 119 120 eleqtrrd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
122 id ⊢ ( 𝑡 = 𝑟 → 𝑡 = 𝑟 )
123 fveq2 ⊢ ( 𝑡 = 𝑟 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑟 ) )
124 123 csbeq1d ⊢ ( 𝑡 = 𝑟 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
125 122 124 eleq12d ⊢ ( 𝑡 = 𝑟 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 ) )
126 125 40 60 rspcdva ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
127 126 adantr ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
128 106 csbeq1d ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
129 127 128 eleqtrrd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
130 potr ⊢ ( ( ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ∧ ( 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ∧ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ∧ 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) ) → ( ( 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) → 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
131 112 113 121 129 130 syl13anc ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) → 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
132 107 111 131 mp2and ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 )
133 106 132 jca ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
134 133 olcd ⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
135 134 ex ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
136 93 98 103 135 ccased ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) ∧ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
137 73 85 136 syl2ani ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
138 simpl ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → 𝑦 = 𝑝 )
139 138 fveq2d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑝 ) )
140 simpr ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → 𝑧 = 𝑟 )
141 140 fveq2d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑟 ) )
142 139 141 breq12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) )
143 139 141 eqeq12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ) )
144 139 csbeq1d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 )
145 138 144 140 breq123d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
146 143 145 anbi12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
147 142 146 orbi12d ⊢ ( ( 𝑦 = 𝑝 ∧ 𝑧 = 𝑟 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
148 147 2 brab2a ⊢ ( 𝑝 𝑇 𝑟 ↔ ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
149 148 biimpri ⊢ ( ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑝 𝑇 𝑟 )
150 61 137 149 syl6an ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → 𝑝 𝑇 𝑟 ) )
151 59 150 jca ⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ¬ 𝑝 𝑇 𝑝 ∧ ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → 𝑝 𝑇 𝑟 ) ) )
152 151 ralrimivvva ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) → ∀ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( ¬ 𝑝 𝑇 𝑝 ∧ ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → 𝑝 𝑇 𝑟 ) ) )
153 df-po ⊢ ( 𝑇 Po ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( ¬ 𝑝 𝑇 𝑝 ∧ ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → 𝑝 𝑇 𝑟 ) ) )
154 152 153 sylibr ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) → 𝑇 Po ∪ 𝑥 ∈ 𝐴 𝐵 )