Theorem weiunpo

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

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

Proof

Step	Hyp	Ref	Expression
1		weiun.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2		weiun.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 2 3 6	weiunlem2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑠 ∈ 𝐴 ∀ 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) )
8	7	simp1d	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
9		simpr1	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
10	8 9	ffvelcdmd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 )
11		sonr	⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 ) → ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) )
12	5 10 11	syl2anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) )
13		csbeq1	⊢ ( 𝑠 = ( 𝐹 ‘ 𝑝 ) → ⦋ 𝑠 / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 )
14		csbeq1	⊢ ( 𝑠 = ( 𝐹 ‘ 𝑝 ) → ⦋ 𝑠 / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
15	13 14	poeq12d	⊢ ( 𝑠 = ( 𝐹 ‘ 𝑝 ) → ( ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ↔ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) )
16		simpl3	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 )
17		nfv	⊢ Ⅎ 𝑠 𝑆 Po 𝐵
18		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝑆
19		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐵
20	18 19	nfpo	⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵
21		csbeq1a	⊢ ( 𝑥 = 𝑠 → 𝑆 = ⦋ 𝑠 / 𝑥 ⦌ 𝑆 )
22		csbeq1a	⊢ ( 𝑥 = 𝑠 → 𝐵 = ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
23	21 22	poeq12d	⊢ ( 𝑥 = 𝑠 → ( 𝑆 Po 𝐵 ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ) )
24	17 20 23	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ↔ ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
25	16 24	sylib	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝑆 Po ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
26	15 25 10	rspcdva	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
27		id	⊢ ( 𝑡 = 𝑝 → 𝑡 = 𝑝 )
28		fveq2	⊢ ( 𝑡 = 𝑝 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑝 ) )
29	28	csbeq1d	⊢ ( 𝑡 = 𝑝 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
30	27 29	eleq12d	⊢ ( 𝑡 = 𝑝 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) )
31	7	simp2d	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
32	30 31 9	rspcdva	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
33		poirr	⊢ ( ( ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ∧ 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) → ¬ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 )
34	26 32 33	syl2anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 )
35	34	intnand	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) )
36		ioran	⊢ ( ¬ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ↔ ( ¬ ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∧ ¬ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
37	12 35 36	sylanbrc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
38	1 2	weiunlem1	⊢ ( 𝑝 𝑇 𝑝 ↔ ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) )
39	38	simprbi	⊢ ( 𝑝 𝑇 𝑝 → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
40	37 39	nsyl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ¬ 𝑝 𝑇 𝑝 )
41		simpr3	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
42	9 41	jca	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
43	1 2	weiunlem1	⊢ ( 𝑝 𝑇 𝑞 ↔ ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) ) )
44	43	simprbi	⊢ ( 𝑝 𝑇 𝑞 → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) )
45	1 2	weiunlem1	⊢ ( 𝑞 𝑇 𝑟 ↔ ( ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
46	45	simprbi	⊢ ( 𝑞 𝑇 𝑟 → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
47		simpr2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
48	8 47	ffvelcdmd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
49	8 41	ffvelcdmd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 )
50		sotr	⊢ ( ( 𝑅 Or 𝐴 ∧ ( ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑟 ) ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) )
51	5 10 48 49 50	syl13anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) )
52		orc	⊢ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
53	51 52	syl6	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
54		simprll	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) )
55		simprr	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) )
56	54 55	eqbrtrd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) )
57	56	orcd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
58	57	ex	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
59		simprl	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) )
60		simprrl	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) )
61	59 60	breqtrd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) )
62	61	orcd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
63	62	ex	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
64		simprll	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) )
65		simprrl	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) )
66	64 65	eqtrd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) )
67		simprlr	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 )
68		simprrr	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 )
69	64	csbeq1d	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 )
70	69	breqd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( 𝑞 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ↔ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
71	68 70	mpbird	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑞 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 )
72	26	adantr	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
73	32	adantr	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
74		id	⊢ ( 𝑡 = 𝑞 → 𝑡 = 𝑞 )
75		fveq2	⊢ ( 𝑡 = 𝑞 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑞 ) )
76	75	csbeq1d	⊢ ( 𝑡 = 𝑞 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
77	74 76	eleq12d	⊢ ( 𝑡 = 𝑞 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) )
78	77 31 47	rspcdva	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
79	78	adantr	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
80	64	csbeq1d	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
81	79 80	eleqtrrd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
82		id	⊢ ( 𝑡 = 𝑟 → 𝑡 = 𝑟 )
83		fveq2	⊢ ( 𝑡 = 𝑟 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑟 ) )
84	83	csbeq1d	⊢ ( 𝑡 = 𝑟 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
85	82 84	eleq12d	⊢ ( 𝑡 = 𝑟 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 ) )
86	85 31 41	rspcdva	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
87	86	adantr	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
88	66	csbeq1d	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝐵 )
89	87 88	eleqtrrd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 )
90		potr	⊢ ( ( ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 Po ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ∧ ( 𝑝 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ∧ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ∧ 𝑟 ∈ ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝐵 ) ) → ( ( 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) → 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
91	72 73 81 89 90	syl13anc	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) → 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
92	67 71 91	mp2and	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 )
93	66 92	jca	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) )
94	93	olcd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) ∧ ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) )
95	94	ex	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
96	53 58 63 95	ccased	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) ∧ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
97	44 46 96	syl2ani	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
98	1 2	weiunlem1	⊢ ( 𝑝 𝑇 𝑟 ↔ ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
99	98	biimpri	⊢ ( ( ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑝 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑝 ⦋ ( 𝐹 ‘ 𝑝 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) → 𝑝 𝑇 𝑟 )
100	42 97 99	syl6an	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → 𝑝 𝑇 𝑟 ) )
101	40 100	jca	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) ∧ ( 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) → ( ¬ 𝑝 𝑇 𝑝 ∧ ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → 𝑝 𝑇 𝑟 ) ) )
102	101	ralrimivvva	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) → ∀ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( ¬ 𝑝 𝑇 𝑝 ∧ ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → 𝑝 𝑇 𝑟 ) ) )
103		df-po	⊢ ( 𝑇 Po ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∀ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( ¬ 𝑝 𝑇 𝑝 ∧ ( ( 𝑝 𝑇 𝑞 ∧ 𝑞 𝑇 𝑟 ) → 𝑝 𝑇 𝑟 ) ) )
104	102 103	sylibr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Po 𝐵 ) → 𝑇 Po ∪ 𝑥 ∈ 𝐴 𝐵 )