Theorem weiunfr 36450

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 3911	. . . . . . . 8 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → ⦋𝑠 / 𝑥⦌𝑆 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆)
2		csbeq1 3911	. . . . . . . 8 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → ⦋𝑠 / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
3	1, 2	freq12d 5658	. . . . . . 7 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → (⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆 Fr ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
4		simpl3 1192	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵)
5		nfv 1912	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑆 Fr 𝐵
6		nfcsb1v 3933	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆
7		nfcsb1v 3933	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐵
8	6, 7	nffr 5662	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵
9		csbeq1a 3922	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝑆 = ⦋𝑠 / 𝑥⦌𝑆)
10		csbeq1a 3922	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝐵 = ⦋𝑠 / 𝑥⦌𝐵)
11	9, 10	freq12d 5658	. . . . . . . . 9 ⊢ (𝑥 = 𝑠 → (𝑆 Fr 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵))
12	5, 8, 11	cbvralw 3304	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ↔ ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵)
13	4, 12	sylib 218	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑠 ∈ 𝐴 ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵)
14		weiun.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
15		weiun.2	. . . . . . . . . . 11 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
16		simpl1 1190	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑅 We 𝐴)
17		simpl2 1191	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑅 Se 𝐴)
18	14, 15, 16, 17	weiunlem2 36446	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
19	18	simp1d 1141	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
20	19	fimassd 6758	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹 “ 𝑟) ⊆ 𝐴)
21		eqid 2735	. . . . . . . . . 10 ⊢ (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)
22		simprl 771	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
23		simprr 773	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ≠ ∅)
24	14, 15, 16, 17, 21, 22, 23	weiunfrlem 36447	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ((℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
25	24	simp1d 1141	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟))
26	20, 25	sseldd 3996	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ 𝐴)
27	3, 13, 26	rspcdva 3623	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆 Fr ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
28		inss2 4246	. . . . . . 7 ⊢ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ⊆ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵
29	28	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ⊆ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
30		vex 3482	. . . . . . . 8 ⊢ 𝑟 ∈ V
31	30	inex1 5323	. . . . . . 7 ⊢ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∈ V
32	31	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∈ V)
33	19	ffund 6741	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → Fun 𝐹)
34		fvelima 6974	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟)) → ∃𝑡 ∈ 𝑟 (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
35	33, 25, 34	syl2anc 584	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑡 ∈ 𝑟 (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
36		simprl 771	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ 𝑟)
37		simplrl 777	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
38	37, 36	sseldd 3996	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
39	18	simp2d 1142	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
40	39	r19.21bi 3249	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
41	38, 40	syldan 591	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
42		simprr 773	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
43	42	csbeq1d 3912	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
44	41, 43	eleqtrd 2841	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
45	36, 44	elind 4210	. . . . . . . 8 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
46	45	ne0d 4348	. . . . . . 7 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ≠ ∅)
47	35, 46	rexlimddv 3159	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ≠ ∅)
48	27, 29, 32, 47	frd 5645	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
49		simprl 771	. . . . . 6 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → 𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
50	49	elin1d 4214	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → 𝑛 ∈ 𝑟)
51		fveq2 6907	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑜 → (𝐹‘𝑡) = (𝐹‘𝑜))
52	51	breq1d 5158	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑜 → ((𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
53	52	notbid 318	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑜 → (¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ ¬ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
54	24	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ((℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
55	54	simp2d 1142	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
56		simpr 484	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑜 ∈ 𝑟)
57	53, 55, 56	rspcdva 3623	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
58		fveqeq2 6916	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑛 → ((𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
59	54	simp3d 1143	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
60		simplrl 777	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
61	58, 59, 60	rspcdva 3623	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
62	61	breq2d 5160	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ↔ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
63	57, 62	mtbird 325	. . . . . . . . 9 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ (𝐹‘𝑜)𝑅(𝐹‘𝑛))
64		breq1 5151	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑜 → (𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛 ↔ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛))
65	64	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑜 → (¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛 ↔ ¬ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛))
66		simprr 773	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
67	66	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
68		simplr 769	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ 𝑟)
69		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑜 → 𝑡 = 𝑜)
70	51	csbeq1d 3912	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑜 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
71	69, 70	eleq12d 2833	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑜 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵))
72	39	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
73	22	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
74	73, 56	sseldd 3996	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
75	74	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
76	71, 72, 75	rspcdva 3623	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
77		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑜) = (𝐹‘𝑛))
78	61	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
79	77, 78	eqtrd 2775	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑜) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
80	79	csbeq1d 3912	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
81	76, 80	eleqtrd 2841	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
82	68, 81	elind 4210	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
83	65, 67, 82	rspcdva 3623	. . . . . . . . . . . 12 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ¬ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
84	79	csbeq1d 3912	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝑆 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆)
85	84	breqd 5159	. . . . . . . . . . . 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 36445	. . . . . . 7 ⊢ (𝑜𝑇𝑛 ↔ ((𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑛 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))))
95	93, 94	sylnibr 329	. . . . . 6 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ 𝑜𝑇𝑛)
96	95	ralrimiva 3144	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛)
97	48, 50, 96	reximssdv 3171	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛)
98	97	ex 412	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
99	98	alrimiv 1925	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ∀𝑟((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
100		df-fr 5641	. 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 1535   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  {crab 3433  Vcvv 3478  ⦋csb 3908   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339  ∪ ciun 4996   class class class wbr 5148  {copab 5210   ↦ cmpt 5231   Fr wfr 5638   Se wse 5639   We wwe 5640   “ cima 5692  Fun wfun 6557  ⟶wf 6559  ‘cfv 6563  ℩crio 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-riota 7388

This theorem is referenced by:  weiunwe  36452