weiunfrlem2 - Mathbox for Matthew House

	Mathbox for Matthew House		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > weiunfrlem2		Structured version Visualization version GIF version

Theorem weiunfrlem2 36381

Description: Lemma for weiunfr 36382. (Contributed by Matthew House, 23-Aug-2025.)

**Hypotheses**
Ref	Expression
weiunfrlem2.1	⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
weiunfrlem2.2	⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
weiunfrlem2.3	⊢ 𝐶 = (℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)

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

Distinct variable groups: 𝑢,𝐴,𝑣,𝑤,𝑥 𝐴,𝑟,𝑤,𝑥,𝑠,𝑡 𝑦,𝐴,𝑧,𝑡,𝑥 𝐵,𝑠,𝑟 𝑢,𝐵,𝑣,𝑤 𝑡,𝐵,𝑦,𝑧 𝑣,𝐶,𝑤 𝑡,𝐶 𝑣,𝐹 𝐹,𝑠,𝑤,𝑡 𝑦,𝐹,𝑧 𝑅,𝑠 𝑢,𝑅,𝑣 𝑅,𝑟,𝑤,𝑡,𝑥 𝑦,𝑅,𝑧 𝑆,𝑟,𝑡 𝑦,𝑆,𝑧 𝑇,𝑟,𝑡 Allowed substitution hints: 𝐵(𝑥) 𝐶(𝑥,𝑦,𝑧,𝑢,𝑠,𝑟) 𝑆(𝑥,𝑤,𝑣,𝑢,𝑠) 𝑇(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢,𝑠) 𝐹(𝑥,𝑢,𝑟)

Proof of Theorem weiunfrlem2 Dummy variables 𝑞 𝑜 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3486	. . . . . . . 8 ⊢ 𝑟 ∈ V
2	1	inex1 5338	. . . . . . 7 ⊢ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∈ V
3	2	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∈ V)
4		weiunfrlem2.1	. . . . . . . . . . . . 13 ⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
5	4	weiunlem1 36376	. . . . . . . . . . . 12 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
6	5	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
7	6	3adantl3 1168	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
8	7	simp1d 1142	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
9	8	fimassd 6767	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐹 “ 𝑟) ⊆ 𝐴)
10		weiunfrlem2.3	. . . . . . . . . . 11 ⊢ 𝐶 = (℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)
11	4, 10	weiunfrlem1 36380	. . . . . . . . . 10 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐶 ∈ (𝐹 “ 𝑟) ∧ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶))
12	11	3adantl3 1168	. . . . . . . . 9 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝐶 ∈ (𝐹 “ 𝑟) ∧ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶))
13	12	simpld 494	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐶 ∈ (𝐹 “ 𝑟))
14	9, 13	sseldd 4003	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → 𝐶 ∈ 𝐴)
15		simpl3 1193	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵)
16		nfiu1 5053	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
17		nfrab1 3458	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}
18		nfv 1913	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 ¬ 𝑣𝑅𝑢
19	17, 18	nfralw 3312	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢
20	19, 17	nfriota 7414	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥(℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)
21	16, 20	nfmpt 5276	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
22	4, 21	nfcxfr 2902	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝐹
23		nfcv 2904	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑟
24	22, 23	nfima 6096	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝐹 “ 𝑟)
25		nfv 1913	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 ¬ 𝑡𝑅𝑠
26	24, 25	nfralw 3312	. . . . . . . . . 10 ⊢ Ⅎ𝑥∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠
27	26, 24	nfriota 7414	. . . . . . . . 9 ⊢ Ⅎ𝑥(℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)
28	10, 27	nfcxfr 2902	. . . . . . . 8 ⊢ Ⅎ𝑥𝐶
29		nfra1 3285	. . . . . . . . 9 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵
30	28	nfcsb1 3939	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝐶 / 𝑥⦌𝑆
31	28	nfcsb1 3939	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝐶 / 𝑥⦌𝐵
32	30, 31	nffr 5673	. . . . . . . . 9 ⊢ Ⅎ𝑥⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵
33	29, 32	nfim 1895	. . . . . . . 8 ⊢ Ⅎ𝑥(∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → ⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵)
34		csbeq1a 3929	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐶 → 𝑆 = ⦋𝐶 / 𝑥⦌𝑆)
35		freq1 5669	. . . . . . . . . . 11 ⊢ (𝑆 = ⦋𝐶 / 𝑥⦌𝑆 → (𝑆 Fr 𝐵 ↔ ⦋𝐶 / 𝑥⦌𝑆 Fr 𝐵))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ (𝑥 = 𝐶 → (𝑆 Fr 𝐵 ↔ ⦋𝐶 / 𝑥⦌𝑆 Fr 𝐵))
37		csbeq1a 3929	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐶 → 𝐵 = ⦋𝐶 / 𝑥⦌𝐵)
38		freq2 5670	. . . . . . . . . . 11 ⊢ (𝐵 = ⦋𝐶 / 𝑥⦌𝐵 → (⦋𝐶 / 𝑥⦌𝑆 Fr 𝐵 ↔ ⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵))
39	37, 38	syl 17	. . . . . . . . . 10 ⊢ (𝑥 = 𝐶 → (⦋𝐶 / 𝑥⦌𝑆 Fr 𝐵 ↔ ⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵))
40	36, 39	bitrd 279	. . . . . . . . 9 ⊢ (𝑥 = 𝐶 → (𝑆 Fr 𝐵 ↔ ⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵))
41	40	imbi2d 340	. . . . . . . 8 ⊢ (𝑥 = 𝐶 → ((∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → 𝑆 Fr 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → ⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵)))
42		rsp 3248	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → (𝑥 ∈ 𝐴 → 𝑆 Fr 𝐵))
43	42	com12 32	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → 𝑆 Fr 𝐵))
44	28, 33, 41, 43	vtoclgaf 3584	. . . . . . 7 ⊢ (𝐶 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 → ⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵))
45	14, 15, 44	sylc 65	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵)
46		inss2 4253	. . . . . . 7 ⊢ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ⊆ ⦋𝐶 / 𝑥⦌𝐵
47	46	a1i 11	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ⊆ ⦋𝐶 / 𝑥⦌𝐵)
48	8	ffund 6750	. . . . . . . 8 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → Fun 𝐹)
49		fvelima 6986	. . . . . . . 8 ⊢ ((Fun 𝐹 ∧ 𝐶 ∈ (𝐹 “ 𝑟)) → ∃𝑜 ∈ 𝑟 (𝐹‘𝑜) = 𝐶)
50	48, 13, 49	syl2anc 583	. . . . . . 7 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑜 ∈ 𝑟 (𝐹‘𝑜) = 𝐶)
51		simprl 770	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → 𝑜 ∈ 𝑟)
52		simplrl 776	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
53	52, 51	sseldd 4003	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → 𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
54	7	simp2d 1143	. . . . . . . . . . . 12 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵)
55	54	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵)
56		id 22	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑜 → 𝑤 = 𝑜)
57		fveq2 6919	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑜 → (𝐹‘𝑤) = (𝐹‘𝑜))
58	57	csbeq1d 3919	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑜 → ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
59	56, 58	eleq12d 2832	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑜 → (𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ↔ 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵))
60	59	rspcv 3627	. . . . . . . . . . 11 ⊢ (𝑜 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → (∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 → 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵))
61	53, 55, 60	sylc 65	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → 𝑜 ∈ ⦋(𝐹‘𝑜) / 𝑥⦌𝐵)
62		csbeq1 3918	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑜) = 𝐶 → ⦋(𝐹‘𝑜) / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐵)
63	62	ad2antll 728	. . . . . . . . . 10 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → ⦋(𝐹‘𝑜) / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐵)
64	61, 63	eleqtrd 2840	. . . . . . . . 9 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → 𝑜 ∈ ⦋𝐶 / 𝑥⦌𝐵)
65	51, 64	elind 4217	. . . . . . . 8 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → 𝑜 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵))
66	65	ne0d 4360	. . . . . . 7 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑜 ∈ 𝑟 ∧ (𝐹‘𝑜) = 𝐶)) → (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ≠ ∅)
67	50, 66	rexlimddv 3163	. . . . . 6 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ≠ ∅)
68		fri 5659	. . . . . 6 ⊢ ((((𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∈ V ∧ ⦋𝐶 / 𝑥⦌𝑆 Fr ⦋𝐶 / 𝑥⦌𝐵) ∧ ((𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ⊆ ⦋𝐶 / 𝑥⦌𝐵 ∧ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ≠ ∅)) → ∃𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵)∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)
69	3, 45, 47, 67, 68	syl22anc 838	. . . . 5 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵)∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)
70		simprl 770	. . . . . 6 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵))
71	70	elin1d 4221	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝑝 ∈ 𝑟)
72	12	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → (𝐶 ∈ (𝐹 “ 𝑟) ∧ ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶))
73	72	simprd 495	. . . . . . . . . . 11 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → ∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶)
74		fveq2 6919	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑡 → (𝐹‘𝑤) = (𝐹‘𝑡))
75	74	breq1d 5179	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑡 → ((𝐹‘𝑤)𝑅𝐶 ↔ (𝐹‘𝑡)𝑅𝐶))
76	75	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑡 → (¬ (𝐹‘𝑤)𝑅𝐶 ↔ ¬ (𝐹‘𝑡)𝑅𝐶))
77	76	rspcv 3627	. . . . . . . . . . 11 ⊢ (𝑡 ∈ 𝑟 → (∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶 → ¬ (𝐹‘𝑡)𝑅𝐶))
78	73, 77	mpan9 506	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → ¬ (𝐹‘𝑡)𝑅𝐶)
79		fveq2 6919	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑝 → (𝐹‘𝑤) = (𝐹‘𝑝))
80	79	breq1d 5179	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑝 → ((𝐹‘𝑤)𝑅𝐶 ↔ (𝐹‘𝑝)𝑅𝐶))
81	80	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑝 → (¬ (𝐹‘𝑤)𝑅𝐶 ↔ ¬ (𝐹‘𝑝)𝑅𝐶))
82	81	rspcv 3627	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ 𝑟 → (∀𝑤 ∈ 𝑟 ¬ (𝐹‘𝑤)𝑅𝐶 → ¬ (𝐹‘𝑝)𝑅𝐶))
83	71, 73, 82	sylc 65	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → ¬ (𝐹‘𝑝)𝑅𝐶)
84	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → (𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ∧ ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤))))
85	84	simp3d 1144	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)))
86	70	elin2d 4222	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝑝 ∈ ⦋𝐶 / 𝑥⦌𝐵)
87		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵)
88	87, 71	sseldd 4003	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
89	14	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝐶 ∈ 𝐴)
90		simpl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = 𝑝 ∧ 𝑣 = 𝐶) → 𝑤 = 𝑝)
91		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 = 𝑝 ∧ 𝑣 = 𝐶) → 𝑣 = 𝐶)
92	91	csbeq1d 3919	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = 𝑝 ∧ 𝑣 = 𝐶) → ⦋𝑣 / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐵)
93	90, 92	eleq12d 2832	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = 𝑝 ∧ 𝑣 = 𝐶) → (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 ↔ 𝑝 ∈ ⦋𝐶 / 𝑥⦌𝐵))
94	90	fveq2d 6923	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑤 = 𝑝 ∧ 𝑣 = 𝐶) → (𝐹‘𝑤) = (𝐹‘𝑝))
95	91, 94	breq12d 5182	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑤 = 𝑝 ∧ 𝑣 = 𝐶) → (𝑣𝑅(𝐹‘𝑤) ↔ 𝐶𝑅(𝐹‘𝑝)))
96	95	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑤 = 𝑝 ∧ 𝑣 = 𝐶) → (¬ 𝑣𝑅(𝐹‘𝑤) ↔ ¬ 𝐶𝑅(𝐹‘𝑝)))
97	93, 96	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ ((𝑤 = 𝑝 ∧ 𝑣 = 𝐶) → ((𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)) ↔ (𝑝 ∈ ⦋𝐶 / 𝑥⦌𝐵 → ¬ 𝐶𝑅(𝐹‘𝑝))))
98	97	rspc2gv 3641	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝐶 ∈ 𝐴) → (∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)) → (𝑝 ∈ ⦋𝐶 / 𝑥⦌𝐵 → ¬ 𝐶𝑅(𝐹‘𝑝))))
99	88, 89, 98	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → (∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵∀𝑣 ∈ 𝐴 (𝑤 ∈ ⦋𝑣 / 𝑥⦌𝐵 → ¬ 𝑣𝑅(𝐹‘𝑤)) → (𝑝 ∈ ⦋𝐶 / 𝑥⦌𝐵 → ¬ 𝐶𝑅(𝐹‘𝑝))))
100	85, 86, 99	mp2d 49	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → ¬ 𝐶𝑅(𝐹‘𝑝))
101		simpll1 1212	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝑅 We 𝐴)
102		weso 5690	. . . . . . . . . . . . . . 15 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝑅 Or 𝐴)
104	8	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → 𝐹:∪ 𝑥 ∈ 𝐴 𝐵⟶𝐴)
105	104, 88	ffvelcdmd 7117	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → (𝐹‘𝑝) ∈ 𝐴)
106		sotrieq2 5641	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ ((𝐹‘𝑝) ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ((𝐹‘𝑝) = 𝐶 ↔ (¬ (𝐹‘𝑝)𝑅𝐶 ∧ ¬ 𝐶𝑅(𝐹‘𝑝))))
107	103, 105, 89, 106	syl12anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → ((𝐹‘𝑝) = 𝐶 ↔ (¬ (𝐹‘𝑝)𝑅𝐶 ∧ ¬ 𝐶𝑅(𝐹‘𝑝))))
108	83, 100, 107	mpbir2and 712	. . . . . . . . . . . 12 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → (𝐹‘𝑝) = 𝐶)
109	108	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → (𝐹‘𝑝) = 𝐶)
110		breq2 5173	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑝) = 𝐶 → ((𝐹‘𝑡)𝑅(𝐹‘𝑝) ↔ (𝐹‘𝑡)𝑅𝐶))
111	110	notbid 318	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑝) = 𝐶 → (¬ (𝐹‘𝑡)𝑅(𝐹‘𝑝) ↔ ¬ (𝐹‘𝑡)𝑅𝐶))
112	109, 111	syl 17	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → (¬ (𝐹‘𝑡)𝑅(𝐹‘𝑝) ↔ ¬ (𝐹‘𝑡)𝑅𝐶))
113	78, 112	mpbird 257	. . . . . . . . 9 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → ¬ (𝐹‘𝑡)𝑅(𝐹‘𝑝))
114		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → 𝑡 ∈ 𝑟)
115	87	sselda 4002	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
116	54	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → ∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵)
117		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑡 → 𝑤 = 𝑡)
118	74	csbeq1d 3919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑡 → ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 = ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
119	117, 118	eleq12d 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = 𝑡 → (𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 ↔ 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵))
120	119	rspcv 3627	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → (∀𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑤 ∈ ⦋(𝐹‘𝑤) / 𝑥⦌𝐵 → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵))
121	115, 116, 120	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
122	121	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → 𝑡 ∈ ⦋(𝐹‘𝑡) / 𝑥⦌𝐵)
123		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → (𝐹‘𝑡) = (𝐹‘𝑝))
124	109	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → (𝐹‘𝑝) = 𝐶)
125	123, 124	eqtrd 2774	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → (𝐹‘𝑡) = 𝐶)
126	125	csbeq1d 3919	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → ⦋(𝐹‘𝑡) / 𝑥⦌𝐵 = ⦋𝐶 / 𝑥⦌𝐵)
127	122, 126	eleqtrd 2840	. . . . . . . . . . . . . 14 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → 𝑡 ∈ ⦋𝐶 / 𝑥⦌𝐵)
128	114, 127	elind 4217	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → 𝑡 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵))
129		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)
130	129	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)
131		breq1 5172	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑡 → (𝑞⦋𝐶 / 𝑥⦌𝑆𝑝 ↔ 𝑡⦋𝐶 / 𝑥⦌𝑆𝑝))
132	131	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑡 → (¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝 ↔ ¬ 𝑡⦋𝐶 / 𝑥⦌𝑆𝑝))
133	132	rspcv 3627	. . . . . . . . . . . . 13 ⊢ (𝑡 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) → (∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝 → ¬ 𝑡⦋𝐶 / 𝑥⦌𝑆𝑝))
134	128, 130, 133	sylc 65	. . . . . . . . . . . 12 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → ¬ 𝑡⦋𝐶 / 𝑥⦌𝑆𝑝)
135	125	csbeq1d 3919	. . . . . . . . . . . . 13 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → ⦋(𝐹‘𝑡) / 𝑥⦌𝑆 = ⦋𝐶 / 𝑥⦌𝑆)
136	135	breqd 5180	. . . . . . . . . . . 12 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → (𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝 ↔ 𝑡⦋𝐶 / 𝑥⦌𝑆𝑝))
137	134, 136	mtbird 325	. . . . . . . . . . 11 ⊢ ((((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) ∧ (𝐹‘𝑡) = (𝐹‘𝑝)) → ¬ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝)
138	137	ex 412	. . . . . . . . . 10 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → ((𝐹‘𝑡) = (𝐹‘𝑝) → ¬ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝))
139		imnan 399	. . . . . . . . . 10 ⊢ (((𝐹‘𝑡) = (𝐹‘𝑝) → ¬ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝) ↔ ¬ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝))
140	138, 139	sylib 218	. . . . . . . . 9 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → ¬ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝))
141		pm4.56 989	. . . . . . . . . 10 ⊢ ((¬ (𝐹‘𝑡)𝑅(𝐹‘𝑝) ∧ ¬ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝)) ↔ ¬ ((𝐹‘𝑡)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝)))
142	141	biimpi 216	. . . . . . . . 9 ⊢ ((¬ (𝐹‘𝑡)𝑅(𝐹‘𝑝) ∧ ¬ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝)) → ¬ ((𝐹‘𝑡)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝)))
143	113, 140, 142	syl2anc 583	. . . . . . . 8 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → ¬ ((𝐹‘𝑡)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝)))
144	143	intnand 488	. . . . . . 7 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → ¬ ((𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑡)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝))))
145		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → 𝑦 = 𝑡)
146	145	fveq2d 6923	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → (𝐹‘𝑦) = (𝐹‘𝑡))
147		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → 𝑧 = 𝑝)
148	147	fveq2d 6923	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → (𝐹‘𝑧) = (𝐹‘𝑝))
149	146, 148	breq12d 5182	. . . . . . . . 9 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝑡)𝑅(𝐹‘𝑝)))
150	146, 148	eqeq12d 2750	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝑡) = (𝐹‘𝑝)))
151	146	csbeq1d 3919	. . . . . . . . . . 11 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝑡) / 𝑥⦌𝑆)
152	145, 151, 147	breq123d 5183	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝))
153	150, 152	anbi12d 631	. . . . . . . . 9 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝)))
154	149, 153	orbi12d 917	. . . . . . . 8 ⊢ ((𝑦 = 𝑡 ∧ 𝑧 = 𝑝) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝑡)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝))))
155		weiunfrlem2.2	. . . . . . . 8 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
156	154, 155	brab2a 5792	. . . . . . 7 ⊢ (𝑡𝑇𝑝 ↔ ((𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑡)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑡) = (𝐹‘𝑝) ∧ 𝑡⦋(𝐹‘𝑡) / 𝑥⦌𝑆𝑝))))
157	144, 156	sylnibr 329	. . . . . 6 ⊢ (((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) ∧ 𝑡 ∈ 𝑟) → ¬ 𝑡𝑇𝑝)
158	157	ralrimiva 3148	. . . . 5 ⊢ ((((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) ∧ (𝑝 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ∧ ∀𝑞 ∈ (𝑟 ∩ ⦋𝐶 / 𝑥⦌𝐵) ¬ 𝑞⦋𝐶 / 𝑥⦌𝑆𝑝)) → ∀𝑡 ∈ 𝑟 ¬ 𝑡𝑇𝑝)
159	69, 71, 158	reximssdv 3175	. . . 4 ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ∧ (𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅)) → ∃𝑝 ∈ 𝑟 ∀𝑡 ∈ 𝑟 ¬ 𝑡𝑇𝑝)
160	159	ex 412	. . 3 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑝 ∈ 𝑟 ∀𝑡 ∈ 𝑟 ¬ 𝑡𝑇𝑝))
161	160	alrimiv 1926	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → ∀𝑟((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑝 ∈ 𝑟 ∀𝑡 ∈ 𝑟 ¬ 𝑡𝑇𝑝))
162		df-fr 5654	. 2 ⊢ (𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑟((𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ≠ ∅) → ∃𝑝 ∈ 𝑟 ∀𝑡 ∈ 𝑟 ¬ 𝑡𝑇𝑝))
163	161, 162	sylibr 234	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 ∧ w3a 1087 ∀wal 1535 = wceq 1537 ∈ wcel 2103 ≠ wne 2942 ∀wral 3063 ∃wrex 3072 {crab 3438 Vcvv 3482 ⦋csb 3915 ∩ cin 3969 ⊆ wss 3970 ∅c0 4347 ∪ ciun 5019 class class class wbr 5169 {copab 5231 ↦ cmpt 5252 Or wor 5610 Fr wfr 5651 Se wse 5652 We wwe 5653 “ cima 5702 Fun wfun 6566 ⟶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: weiunfr 36382

W3C validator