Theorem weiunfr 36409

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 3884	. . . . . . . 8 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → ⦋𝑠 / 𝑥⦌𝑆 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆)
2		csbeq1 3884	. . . . . . . 8 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → ⦋𝑠 / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
3	1, 2	freq12d 5636	. . . . . . 7 ⊢ (𝑠 = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) → (⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵 ↔ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆 Fr ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
4		simpl3 1193	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵)
5		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑆 Fr 𝐵
6		nfcsb1v 3905	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆
7		nfcsb1v 3905	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝐵
8	6, 7	nffr 5640	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵
9		csbeq1a 3895	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝑆 = ⦋𝑠 / 𝑥⦌𝑆)
10		csbeq1a 3895	. . . . . . . . . 10 ⊢ (𝑥 = 𝑠 → 𝐵 = ⦋𝑠 / 𝑥⦌𝐵)
11	9, 10	freq12d 5636	. . . . . . . . 9 ⊢ (𝑥 = 𝑠 → (𝑆 Fr 𝐵 ↔ ⦋𝑠 / 𝑥⦌𝑆 Fr ⦋𝑠 / 𝑥⦌𝐵))
12	5, 8, 11	cbvralw 3290	. . . . . . . 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 36405	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ∧ ∀𝑠 ∈ 𝐴 ∀𝑡 ∈ ⦋ 𝑠 / 𝑥⦌𝐵 ¬ 𝑠𝑅(𝐹‘𝑡)))
19	18	simp1d 1142	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
20	19	fimassd 6738	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹 “ 𝑟) ⊆ 𝐴)
21		eqid 2734	. . . . . . . . . 10 ⊢ (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)
22		simprl 770	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
23		simprr 772	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝑟 ≠ ∅)
24	14, 15, 16, 17, 21, 22, 23	weiunfrlem 36406	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ((℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟) ∧ ∀𝑡 ∈ 𝑟 ¬ (𝐹‘𝑡)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∧ ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
25	24	simp1d 1142	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ (𝐹 “ 𝑟))
26	20, 25	sseldd 3966	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ∈ 𝐴)
27	3, 13, 26	rspcdva 3607	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆 Fr ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
28		inss2 4220	. . . . . . 7 ⊢ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ⊆ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵
29	28	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ⊆ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
30		vex 3468	. . . . . . . 8 ⊢ 𝑟 ∈ V
31	30	inex1 5299	. . . . . . 7 ⊢ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∈ V
32	31	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∈ V)
33	19	ffund 6721	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → Fun 𝐹)
34		fvelima 6955	. . . . . . . 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 3966	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
39	18	simp2d 1143	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
40	39	r19.21bi 3238	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
41	38, 40	syldan 591	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
42		simprr 772	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
43	42	csbeq1d 3885	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
44	41, 43	eleqtrd 2835	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
45	36, 44	elind 4182	. . . . . . . 8 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → 𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
46	45	ne0d 4324	. . . . . . 7 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑡 ∈ 𝑟 ∧ (𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ≠ ∅)
47	35, 46	rexlimddv 3148	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ≠ ∅)
48	27, 29, 32, 47	frd 5623	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
49		simprl 770	. . . . . 6 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → 𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
50	49	elin1d 4186	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → 𝑛 ∈ 𝑟)
51		fveq2 6887	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑜 → (𝐹‘𝑡) = (𝐹‘𝑜))
52	51	breq1d 5135	. . . . . . . . . . . 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 3607	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
58		fveqeq2 6896	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑛 → ((𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) ↔ (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
59	54	simp3d 1144	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ∀𝑡 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)(𝐹‘𝑡) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
60		simplrl 776	. . . . . . . . . . . 12 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
61	58, 59, 60	rspcdva 3607	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
62	61	breq2d 5137	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ↔ (𝐹‘𝑜)𝑅(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝)))
63	57, 62	mtbird 325	. . . . . . . . 9 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ (𝐹‘𝑜)𝑅(𝐹‘𝑛))
64		breq1 5128	. . . . . . . . . . . . . 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 3885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 𝑜 → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
71	69, 70	eleq12d 2827	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 𝑜 → (𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 ↔ 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵))
72	39	ad3antrrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ∀𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
73	22	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
74	73, 56	sseldd 3966	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
75	74	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
76	71, 72, 75	rspcdva 3607	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
77		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑜) = (𝐹‘𝑛))
78	61	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑛) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
79	77, 78	eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → (𝐹‘𝑜) = (℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝))
80	79	csbeq1d 3885	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝐵 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
81	76, 80	eleqtrd 2835	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵)
82	68, 81	elind 4182	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → 𝑜 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵))
83	65, 67, 82	rspcdva 3607	. . . . . . . . . . . 12 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ¬ 𝑜⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)
84	79	csbeq1d 3885	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) ∧ (𝐹‘𝑜) = (𝐹‘𝑛)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝑆 = ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆)
85	84	breqd 5136	. . . . . . . . . . . 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 36404	. . . . . . 7 ⊢ (𝑜𝑇𝑛 ↔ ((𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑛 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑛) ∨ ((𝐹‘𝑜) = (𝐹‘𝑛) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑥⦌𝑆𝑛))))
95	93, 94	sylnibr 329	. . . . . 6 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) ∧ 𝑜 ∈ 𝑟) → ¬ 𝑜𝑇𝑛)
96	95	ralrimiva 3133	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑛 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ∧ ∀𝑚 ∈ (𝑟 ∩ ⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝐵) ¬ 𝑚⦋(℩𝑝 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑝) / 𝑥⦌𝑆𝑛)) → ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛)
97	48, 50, 96	reximssdv 3160	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛)
98	97	ex 412	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
99	98	alrimiv 1926	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ∀𝑟((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑛 ∈ 𝑟 ∀𝑜 ∈ 𝑟 ¬ 𝑜𝑇𝑛))
100		df-fr 5619	. 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 1537   = wceq 1539   ∈ wcel 2107   ≠ wne 2931  ∀wral 3050  ∃wrex 3059  {crab 3420  Vcvv 3464  ⦋csb 3881   ∩ cin 3932   ⊆ wss 3933  ∅c0 4315  ∪ ciun 4973   class class class wbr 5125  {copab 5187   ↦ cmpt 5207   Fr wfr 5616   Se wse 5617   We wwe 5618   “ cima 5670  Fun wfun 6536  ⟶wf 6538  ‘cfv 6542  ℩crio 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pr 5414

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-iun 4975  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-po 5574  df-so 5575  df-fr 5619  df-se 5620  df-we 5621  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-riota 7371

This theorem is referenced by:  weiunwe  36411