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	weiunval	⊢ ( 𝑞 𝑇 𝑟 ↔ ( ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑟 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑟 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑟 ) ) ) )
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	weiunlem	⊢ ( ( ( 𝑅 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	weiunval	⊢ ( 𝑟 𝑇 𝑞 ↔ ( ( 𝑟 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑟 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∨ ( ( 𝐹 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑞 ) ∧ 𝑟 ⦋ ( 𝐹 ‘ 𝑟 ) / 𝑥 ⦌ 𝑆 𝑞 ) ) ) )
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 ∪ 𝑥 ∈ 𝐴 𝐵 )