Theorem weiunfr 36382

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

Hypotheses

Ref	Expression
weiunfr.1	⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
weiunfr.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		weiunfr.1	. . . 4 ⊢ 𝐹 = (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢))
2		breq2 5173	. . . . . . . . 9 ⊢ (𝑢 = 𝑚 → (𝑣𝑅𝑢 ↔ 𝑣𝑅𝑚))
3	2	notbid 318	. . . . . . . 8 ⊢ (𝑢 = 𝑚 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑚))
4	3	ralbidv 3180	. . . . . . 7 ⊢ (𝑢 = 𝑚 → (∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑚))
5	4	cbvriotavw 7411	. . . . . 6 ⊢ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) = (℩𝑚 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑚)
6		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑥𝐴
7		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑙𝐴
8		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑙 𝑤 ∈ 𝐵
9		nfcsb1v 3940	. . . . . . . . . 10 ⊢ Ⅎ𝑥⦋𝑙 / 𝑥⦌𝐵
10	9	nfcri 2895	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑤 ∈ ⦋𝑙 / 𝑥⦌𝐵
11		csbeq1a 3929	. . . . . . . . . 10 ⊢ (𝑥 = 𝑙 → 𝐵 = ⦋𝑙 / 𝑥⦌𝐵)
12	11	eleq2d 2824	. . . . . . . . 9 ⊢ (𝑥 = 𝑙 → (𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋𝑙 / 𝑥⦌𝐵))
13	6, 7, 8, 10, 12	cbvrabw 3475	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} = {𝑙 ∈ 𝐴 ∣ 𝑤 ∈ ⦋𝑙 / 𝑥⦌𝐵}
14		eleq1w 2821	. . . . . . . . 9 ⊢ (𝑤 = 𝑘 → (𝑤 ∈ ⦋𝑙 / 𝑥⦌𝐵 ↔ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵))
15	14	rabbidv 3446	. . . . . . . 8 ⊢ (𝑤 = 𝑘 → {𝑙 ∈ 𝐴 ∣ 𝑤 ∈ ⦋𝑙 / 𝑥⦌𝐵} = {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵})
16	13, 15	eqtrid 2786	. . . . . . 7 ⊢ (𝑤 = 𝑘 → {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} = {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵})
17		breq1 5172	. . . . . . . . . 10 ⊢ (𝑣 = 𝑛 → (𝑣𝑅𝑚 ↔ 𝑛𝑅𝑚))
18	17	notbid 318	. . . . . . . . 9 ⊢ (𝑣 = 𝑛 → (¬ 𝑣𝑅𝑚 ↔ ¬ 𝑛𝑅𝑚))
19	18	adantl 481	. . . . . . . 8 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑛) → (¬ 𝑣𝑅𝑚 ↔ ¬ 𝑛𝑅𝑚))
20	16	adantr 480	. . . . . . . 8 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑛) → {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} = {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵})
21	19, 20	cbvraldva2 3351	. . . . . . 7 ⊢ (𝑤 = 𝑘 → (∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑚 ↔ ∀𝑛 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵} ¬ 𝑛𝑅𝑚))
22	16, 21	riotaeqbidv 7404	. . . . . 6 ⊢ (𝑤 = 𝑘 → (℩𝑚 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑚) = (℩𝑚 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵}∀𝑛 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵} ¬ 𝑛𝑅𝑚))
23	5, 22	eqtrid 2786	. . . . 5 ⊢ (𝑤 = 𝑘 → (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢) = (℩𝑚 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵}∀𝑛 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵} ¬ 𝑛𝑅𝑚))
24	23	cbvmptv 5282	. . . 4 ⊢ (𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑢 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵}∀𝑣 ∈ {𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵} ¬ 𝑣𝑅𝑢)) = (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑚 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵}∀𝑛 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵} ¬ 𝑛𝑅𝑚))
25		nfcv 2904	. . . . . 6 ⊢ Ⅎ𝑙𝐵
26	25, 9, 11	cbviun 5062	. . . . 5 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵
27	26	mpteq1i 5265	. . . 4 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ (℩𝑚 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵}∀𝑛 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵} ¬ 𝑛𝑅𝑚)) = (𝑘 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵 ↦ (℩𝑚 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵}∀𝑛 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵} ¬ 𝑛𝑅𝑚))
28	1, 24, 27	3eqtri 2766	. . 3 ⊢ 𝐹 = (𝑘 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵 ↦ (℩𝑚 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵}∀𝑛 ∈ {𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋𝑙 / 𝑥⦌𝐵} ¬ 𝑛𝑅𝑚))
29		weiunfr.2	. . . 4 ⊢ 𝑇 = {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))}
30		simpl 482	. . . . . . . 8 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → 𝑦 = 𝑜)
31	26	a1i 11	. . . . . . . 8 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵)
32	30, 31	eleq12d 2832	. . . . . . 7 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵))
33		simpr 484	. . . . . . . 8 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → 𝑧 = 𝑝)
34	33, 31	eleq12d 2832	. . . . . . 7 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵))
35	32, 34	anbi12d 631	. . . . . 6 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ↔ (𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵 ∧ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵)))
36	30	fveq2d 6923	. . . . . . . 8 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → (𝐹‘𝑦) = (𝐹‘𝑜))
37	33	fveq2d 6923	. . . . . . . 8 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → (𝐹‘𝑧) = (𝐹‘𝑝))
38	36, 37	breq12d 5182	. . . . . . 7 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ↔ (𝐹‘𝑜)𝑅(𝐹‘𝑝)))
39	36, 37	eqeq12d 2750	. . . . . . . 8 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝐹‘𝑜) = (𝐹‘𝑝)))
40	36	csbeq1d 3919	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝑜) / 𝑥⦌𝑆)
41		csbcow 3930	. . . . . . . . . 10 ⊢ ⦋(𝐹‘𝑜) / 𝑙⦌⦋𝑙 / 𝑥⦌𝑆 = ⦋(𝐹‘𝑜) / 𝑥⦌𝑆
42	40, 41	eqtr4di 2792	. . . . . . . . 9 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → ⦋(𝐹‘𝑦) / 𝑥⦌𝑆 = ⦋(𝐹‘𝑜) / 𝑙⦌⦋𝑙 / 𝑥⦌𝑆)
43	30, 42, 33	breq123d 5183	. . . . . . . 8 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → (𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧 ↔ 𝑜⦋(𝐹‘𝑜) / 𝑙⦌⦋𝑙 / 𝑥⦌𝑆𝑝))
44	39, 43	anbi12d 631	. . . . . . 7 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → (((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧) ↔ ((𝐹‘𝑜) = (𝐹‘𝑝) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑙⦌⦋𝑙 / 𝑥⦌𝑆𝑝)))
45	38, 44	orbi12d 917	. . . . . 6 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → (((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)) ↔ ((𝐹‘𝑜)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑜) = (𝐹‘𝑝) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑙⦌⦋𝑙 / 𝑥⦌𝑆𝑝))))
46	35, 45	anbi12d 631	. . . . 5 ⊢ ((𝑦 = 𝑜 ∧ 𝑧 = 𝑝) → (((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧))) ↔ ((𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵 ∧ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑜) = (𝐹‘𝑝) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑙⦌⦋𝑙 / 𝑥⦌𝑆𝑝)))))
47	46	cbvopabv 5242	. . . 4 ⊢ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ ((𝐹‘𝑦)𝑅(𝐹‘𝑧) ∨ ((𝐹‘𝑦) = (𝐹‘𝑧) ∧ 𝑦⦋(𝐹‘𝑦) / 𝑥⦌𝑆𝑧)))} = {⟨𝑜, 𝑝⟩ ∣ ((𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵 ∧ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑜) = (𝐹‘𝑝) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑙⦌⦋𝑙 / 𝑥⦌𝑆𝑝)))}
48	29, 47	eqtri 2762	. . 3 ⊢ 𝑇 = {⟨𝑜, 𝑝⟩ ∣ ((𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵 ∧ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵) ∧ ((𝐹‘𝑜)𝑅(𝐹‘𝑝) ∨ ((𝐹‘𝑜) = (𝐹‘𝑝) ∧ 𝑜⦋(𝐹‘𝑜) / 𝑙⦌⦋𝑙 / 𝑥⦌𝑆𝑝)))}
49		breq1 5172	. . . . . . 7 ⊢ (𝑞 = 𝑡 → (𝑞𝑅𝑠 ↔ 𝑡𝑅𝑠))
50	49	notbid 318	. . . . . 6 ⊢ (𝑞 = 𝑡 → (¬ 𝑞𝑅𝑠 ↔ ¬ 𝑡𝑅𝑠))
51	50	cbvralvw 3238	. . . . 5 ⊢ (∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑠 ↔ ∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)
52	51	a1i 11	. . . 4 ⊢ (𝑠 ∈ (𝐹 “ 𝑟) → (∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑠 ↔ ∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠))
53	52	riotabiia 7422	. . 3 ⊢ (℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑞 ∈ (𝐹 “ 𝑟) ¬ 𝑞𝑅𝑠) = (℩𝑠 ∈ (𝐹 “ 𝑟)∀𝑡 ∈ (𝐹 “ 𝑟) ¬ 𝑡𝑅𝑠)
54	28, 48, 53	weiunfrlem2 36381	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝑆 Fr ⦋𝑙 / 𝑥⦌𝐵) → 𝑇 Fr ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵)
55		nfv 1913	. . . 4 ⊢ Ⅎ𝑙 𝑆 Fr 𝐵
56		nfcsb1v 3940	. . . . 5 ⊢ Ⅎ𝑥⦋𝑙 / 𝑥⦌𝑆
57	56, 9	nffr 5673	. . . 4 ⊢ Ⅎ𝑥⦋𝑙 / 𝑥⦌𝑆 Fr ⦋𝑙 / 𝑥⦌𝐵
58		csbeq1a 3929	. . . . . 6 ⊢ (𝑥 = 𝑙 → 𝑆 = ⦋𝑙 / 𝑥⦌𝑆)
59		freq1 5669	. . . . . 6 ⊢ (𝑆 = ⦋𝑙 / 𝑥⦌𝑆 → (𝑆 Fr 𝐵 ↔ ⦋𝑙 / 𝑥⦌𝑆 Fr 𝐵))
60	58, 59	syl 17	. . . . 5 ⊢ (𝑥 = 𝑙 → (𝑆 Fr 𝐵 ↔ ⦋𝑙 / 𝑥⦌𝑆 Fr 𝐵))
61		freq2 5670	. . . . . 6 ⊢ (𝐵 = ⦋𝑙 / 𝑥⦌𝐵 → (⦋𝑙 / 𝑥⦌𝑆 Fr 𝐵 ↔ ⦋𝑙 / 𝑥⦌𝑆 Fr ⦋𝑙 / 𝑥⦌𝐵))
62	11, 61	syl 17	. . . . 5 ⊢ (𝑥 = 𝑙 → (⦋𝑙 / 𝑥⦌𝑆 Fr 𝐵 ↔ ⦋𝑙 / 𝑥⦌𝑆 Fr ⦋𝑙 / 𝑥⦌𝐵))
63	60, 62	bitrd 279	. . . 4 ⊢ (𝑥 = 𝑙 → (𝑆 Fr 𝐵 ↔ ⦋𝑙 / 𝑥⦌𝑆 Fr ⦋𝑙 / 𝑥⦌𝐵))
64	55, 57, 63	cbvralw 3307	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ↔ ∀𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝑆 Fr ⦋𝑙 / 𝑥⦌𝐵)
65	64	3anbi3i 1159	. 2 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) ↔ (𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝑆 Fr ⦋𝑙 / 𝑥⦌𝐵))
66		freq2 5670	. . 3 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵 → (𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑇 Fr ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵))
67	26, 66	ax-mp 5	. 2 ⊢ (𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑇 Fr ∪ 𝑙 ∈ 𝐴 ⦋𝑙 / 𝑥⦌𝐵)
68	54, 65, 67	3imtr4i 292	1 ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑆 Fr 𝐵) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1087   = wceq 1537   ∈ wcel 2103  ∀wral 3063  {crab 3438  ⦋csb 3915  ∪ ciun 5019   class class class wbr 5169  {copab 5231   ↦ cmpt 5252   Fr wfr 5651   Se wse 5652   We wwe 5653   “ cima 5702  ‘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:  weiunwe  36384