Theorem weiunpo 36378

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.)

Hypotheses

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

Assertion

Ref	Expression
weiunpo	⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Po 𝐵) → 𝑇 Po ∪ 𝑥 ∈ 𝐴 𝐵)

Distinct variable groups:   𝑢,𝐴,𝑣,𝑤,𝑥   𝑦,𝐴,𝑧,𝑥   𝑢,𝐵,𝑣,𝑤   𝑦,𝐵,𝑧   𝑦,𝐹,𝑧   𝑢,𝑅,𝑣,𝑤   𝑦,𝑅,𝑧   𝑦,𝑆,𝑧

Allowed substitution hints:   𝐵(𝑥)   𝑅(𝑥)   𝑆(𝑥,𝑤,𝑣,𝑢)   𝑇(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝐹(𝑥,𝑤,𝑣,𝑢)

Proof of Theorem weiunpo

Dummy variables 𝑝 𝑠 𝑡 𝑞 𝑟 are mutually distinct and distinct from all other variables.

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537   ∈ wcel 2103  ∀wral 3063  {crab 3438  ⦋csb 3915  ∪ ciun 5019   class class class wbr 5169  {copab 5231   ↦ cmpt 5252   Po wpo 5609   Or wor 5610   Se wse 5652   We wwe 5653  ⟶wf 6568  ‘cfv 6572  ℩crio 7400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-sep 5320  ax-nul 5327  ax-pr 5450

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3383  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-po 5611  df-so 5612  df-fr 5654  df-se 5655  df-we 5656  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-fv 6580  df-riota 7401

This theorem is referenced by:  weiunso  36379