Theorem weiunfr 36455

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

Hypotheses

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

Assertion

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

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

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

Proof of Theorem weiunfr

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

Step	Hyp	Ref	Expression
1		csbeq1 3865	. . . . . . . 8 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → ⦋𝑠 / 𝑥⦌𝑆 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆)
2		csbeq1 3865	. . . . . . . 8 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → ⦋𝑠 / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
3	1, 2	freq12d 5607	. . . . . . 7 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → (⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆 Fr ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
4		simpl3 1194	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵)
5		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑆 Fr 𝐵
6		nfcsb1v 3886	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆
7		nfcsb1v 3886	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐵
8	6, 7	nffr 5611	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵
9		csbeq1a 3876	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝑆 = ⦋𝑠 / 𝑥⦌𝑆)
10		csbeq1a 3876	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝐵 = ⦋𝑠 / 𝑥⦌𝐵)
11	9, 10	freq12d 5607	. . . . . . . . 9 ⊢ (𝑥 = 𝑠 → (𝑆 Fr 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵))
12	5, 8, 11	cbvralw 3280	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ↔ ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵)
13	4, 12	sylib 218	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵)
14		weiun.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
15		weiun.2	. . . . . . . . . . 11 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
16		simpl1 1192	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑅 We 𝐴)
17		simpl2 1193	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑅 Se 𝐴)
18	14, 15, 16, 17	weiunlem2 36451	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
19	18	simp1d 1142	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
20	19	fimassd 6709	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹 “ 𝑟) ⊆ 𝐴)
21		eqid 2729	. . . . . . . . . 10 ⊢ (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)
22		simprl 770	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
23		simprr 772	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ≠ ∅)
24	14, 15, 16, 17, 21, 22, 23	weiunfrlem 36452	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ((℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
25	24	simp1d 1142	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟))
26	20, 25	sseldd 3947	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ 𝐴)
27	3, 13, 26	rspcdva 3589	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆 Fr ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
28		inss2 4201	. . . . . . 7 ⊢ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ⊆ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵
29	28	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ⊆ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
30		vex 3451	. . . . . . . 8 ⊢ 𝑟 ∈ V
31	30	inex1 5272	. . . . . . 7 ⊢ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∈ V
32	31	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∈ V)
33	19	ffund 6692	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → Fun 𝐹)
34		fvelima 6926	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟)) → ∃𝑡 ∈ 𝑟 (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
35	33, 25, 34	syl2anc 584	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑡 ∈ 𝑟 (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
36		simprl 770	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ 𝑟)
37		simplrl 776	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
38	37, 36	sseldd 3947	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
39	18	simp2d 1143	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
40	39	r19.21bi 3229	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
41	38, 40	syldan 591	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
42		simprr 772	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
43	42	csbeq1d 3866	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
44	41, 43	eleqtrd 2830	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
45	36, 44	elind 4163	. . . . . . . 8 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
46	45	ne0d 4305	. . . . . . 7 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ≠ ∅)
47	35, 46	rexlimddv 3140	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ≠ ∅)
48	27, 29, 32, 47	frd 5595	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
49		simprl 770	. . . . . 6 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → 𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
50	49	elin1d 4167	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → 𝑛 ∈ 𝑟)
51		fveq2 6858	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑜 → (𝐹‘𝑡) = (𝐹‘𝑜))
52	51	breq1d 5117	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑜 → ((𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
53	52	notbid 318	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑜 → (¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ ¬ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
54	24	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ((℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
55	54	simp2d 1143	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
56		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑜 ∈ 𝑟)
57	53, 55, 56	rspcdva 3589	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
58		fveqeq2 6867	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑛 → ((𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
59	54	simp3d 1144	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
60		simplrl 776	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
61	58, 59, 60	rspcdva 3589	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
62	61	breq2d 5119	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ↔ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
63	57, 62	mtbird 325	. . . . . . . . 9 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ (𝐹‘𝑜)𝑅(𝐹‘𝑛))
64		breq1 5110	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑜 → (𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛 ↔ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛))
65	64	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑜 → (¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛 ↔ ¬ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛))
66		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
67	66	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
68		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ 𝑟)
69		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑜 → 𝑡 = 𝑜)
70	51	csbeq1d 3866	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑜 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
71	69, 70	eleq12d 2822	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑜 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵))
72	39	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
73	22	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
74	73, 56	sseldd 3947	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
75	74	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
76	71, 72, 75	rspcdva 3589	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
77		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑜) = (𝐹‘𝑛))
78	61	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
79	77, 78	eqtrd 2764	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑜) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
80	79	csbeq1d 3866	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
81	76, 80	eleqtrd 2830	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
82	68, 81	elind 4163	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
83	65, 67, 82	rspcdva 3589	. . . . . . . . . . . 12 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ¬ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
84	79	csbeq1d 3866	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝑆 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆)
85	84	breqd 5118	. . . . . . . . . . . 12 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛 ↔ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛))
86	83, 85	mtbird 325	. . . . . . . . . . 11 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ¬ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)
87	86	ex 412	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ((𝐹‘𝑜) = (𝐹‘𝑛) → ¬ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))
88		imnan 399	. . . . . . . . . 10 ⊢ (((𝐹‘𝑜) = (𝐹‘𝑛) → ¬ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛) ↔ ¬ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))
89	87, 88	sylib 218	. . . . . . . . 9 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))
90		pm4.56 990	. . . . . . . . . 10 ⊢ ((¬ (𝐹‘𝑜)𝑅(𝐹‘𝑛) ∧ ¬ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)) ↔ ¬ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)))
91	90	biimpi 216	. . . . . . . . 9 ⊢ ((¬ (𝐹‘𝑜)𝑅(𝐹‘𝑛) ∧ ¬ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)) → ¬ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)))
92	63, 89, 91	syl2anc 584	. . . . . . . 8 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)))
93	92	intnand 488	. . . . . . 7 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ ((𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑛 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))))
94	14, 15	weiunlem1 36450	. . . . . . 7 ⊢ (𝑜𝑇𝑛 ↔ ((𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑛 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))))
95	93, 94	sylnibr 329	. . . . . 6 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ 𝑜𝑇𝑛)
96	95	ralrimiva 3125	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛)
97	48, 50, 96	reximssdv 3151	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛)
98	97	ex 412	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
99	98	alrimiv 1927	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ∀𝑟((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
100		df-fr 5591	. 2 ⊢ (𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑟((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
101	99, 100	sylibr 234	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3405  Vcvv 3447  ⦋csb 3862   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  ∪ ciun 4955   class class class wbr 5107  {copab 5169   ↦ cmpt 5188   Fr wfr 5588   Se wse 5589   We wwe 5590   “ cima 5641  Fun wfun 6505  ⟶wf 6507  ‘cfv 6511  ℩crio 7343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-riota 7344

This theorem is referenced by:  weiunwe  36457