Theorem weiunfr 36433

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 3924	. . . . . . . 8 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → ⦋𝑠 / 𝑥⦌𝑆 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆)
2		csbeq1 3924	. . . . . . . 8 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → ⦋𝑠 / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
3	1, 2	freq12d 5669	. . . . . . 7 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → (⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆 Fr ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
4		simpl3 1193	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵)
5		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑆 Fr 𝐵
6		nfcsb1v 3946	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆
7		nfcsb1v 3946	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐵
8	6, 7	nffr 5673	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵
9		csbeq1a 3935	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝑆 = ⦋𝑠 / 𝑥⦌𝑆)
10		csbeq1a 3935	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝐵 = ⦋𝑠 / 𝑥⦌𝐵)
11	9, 10	freq12d 5669	. . . . . . . . 9 ⊢ (𝑥 = 𝑠 → (𝑆 Fr 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵))
12	5, 8, 11	cbvralw 3312	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ↔ ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵)
13	4, 12	sylib 218	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵)
14		weiun.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
15		weiun.2	. . . . . . . . . . 11 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
16		simpl1 1191	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑅 We 𝐴)
17		simpl2 1192	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑅 Se 𝐴)
18	14, 15, 16, 17	weiunlem2 36429	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
19	18	simp1d 1142	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
20	19	fimassd 6768	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹 “ 𝑟) ⊆ 𝐴)
21		eqid 2740	. . . . . . . . . 10 ⊢ (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)
22		simprl 770	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
23		simprr 772	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ≠ ∅)
24	14, 15, 16, 17, 21, 22, 23	weiunfrlem 36430	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ((℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
25	24	simp1d 1142	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟))
26	20, 25	sseldd 4009	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ 𝐴)
27	3, 13, 26	rspcdva 3636	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆 Fr ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
28		inss2 4259	. . . . . . 7 ⊢ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ⊆ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵
29	28	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ⊆ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
30		vex 3492	. . . . . . . 8 ⊢ 𝑟 ∈ V
31	30	inex1 5335	. . . . . . 7 ⊢ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∈ V
32	31	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∈ V)
33	19	ffund 6751	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → Fun 𝐹)
34		fvelima 6987	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟)) → ∃𝑡 ∈ 𝑟 (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
35	33, 25, 34	syl2anc 583	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑡 ∈ 𝑟 (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
36		simprl 770	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ 𝑟)
37		simplrl 776	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
38	37, 36	sseldd 4009	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
39	18	simp2d 1143	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
40	39	r19.21bi 3257	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
41	38, 40	syldan 590	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
42		simprr 772	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
43	42	csbeq1d 3925	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
44	41, 43	eleqtrd 2846	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
45	36, 44	elind 4223	. . . . . . . 8 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
46	45	ne0d 4365	. . . . . . 7 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ≠ ∅)
47	35, 46	rexlimddv 3167	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ≠ ∅)
48	27, 29, 32, 47	frd 5656	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
49		simprl 770	. . . . . 6 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → 𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
50	49	elin1d 4227	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → 𝑛 ∈ 𝑟)
51		fveq2 6920	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑜 → (𝐹‘𝑡) = (𝐹‘𝑜))
52	51	breq1d 5176	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑜 → ((𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
53	52	notbid 318	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑜 → (¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ ¬ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
54	24	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ((℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
55	54	simp2d 1143	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
56		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑜 ∈ 𝑟)
57	53, 55, 56	rspcdva 3636	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
58		fveqeq2 6929	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑛 → ((𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
59	54	simp3d 1144	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
60		simplrl 776	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
61	58, 59, 60	rspcdva 3636	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
62	61	breq2d 5178	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ↔ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
63	57, 62	mtbird 325	. . . . . . . . 9 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ (𝐹‘𝑜)𝑅(𝐹‘𝑛))
64		breq1 5169	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑜 → (𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛 ↔ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛))
65	64	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑜 → (¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛 ↔ ¬ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛))
66		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
67	66	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
68		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ 𝑟)
69		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑜 → 𝑡 = 𝑜)
70	51	csbeq1d 3925	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑜 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
71	69, 70	eleq12d 2838	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑜 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵))
72	39	ad3antrrr 729	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
73	22	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
74	73, 56	sseldd 4009	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
75	74	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
76	71, 72, 75	rspcdva 3636	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
77		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑜) = (𝐹‘𝑛))
78	61	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
79	77, 78	eqtrd 2780	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑜) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
80	79	csbeq1d 3925	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
81	76, 80	eleqtrd 2846	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
82	68, 81	elind 4223	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
83	65, 67, 82	rspcdva 3636	. . . . . . . . . . . 12 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ¬ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
84	79	csbeq1d 3925	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝑆 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆)
85	84	breqd 5177	. . . . . . . . . . . 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 989	. . . . . . . . . 10 ⊢ ((¬ (𝐹‘𝑜)𝑅(𝐹‘𝑛) ∧ ¬ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)) ↔ ¬ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)))
91	90	biimpi 216	. . . . . . . . 9 ⊢ ((¬ (𝐹‘𝑜)𝑅(𝐹‘𝑛) ∧ ¬ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)) → ¬ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)))
92	63, 89, 91	syl2anc 583	. . . . . . . 8 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛)))
93	92	intnand 488	. . . . . . 7 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ ((𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑛 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))))
94	14, 15	weiunlem1 36428	. . . . . . 7 ⊢ (𝑜𝑇𝑛 ↔ ((𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑛 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))))
95	93, 94	sylnibr 329	. . . . . 6 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ 𝑜𝑇𝑛)
96	95	ralrimiva 3152	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛)
97	48, 50, 96	reximssdv 3179	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛)
98	97	ex 412	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
99	98	alrimiv 1926	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ∀𝑟((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
100		df-fr 5652	. 2 ⊢ (𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑟((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
101	99, 100	sylibr 234	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 846   ∧ w3a 1087  ∀wal 1535   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  {crab 3443  Vcvv 3488  ⦋csb 3921   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  ∪ ciun 5015   class class class wbr 5166  {copab 5228   ↦ cmpt 5249   Fr wfr 5649   Se wse 5650   We wwe 5651   “ cima 5703  Fun wfun 6567  ⟶wf 6569  ‘cfv 6573  ℩crio 7403

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 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

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 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-riota 7404

This theorem is referenced by:  weiunwe  36435