Theorem weiunfr

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)

	Ref	Expression
Hypotheses	weiunfr.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
	weiunfr.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
Assertion	weiunfr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		weiunfr.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2		weiunfr.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
3		breq2	⊢ ( 𝑢 = 𝑚 → ( 𝑣 𝑅 𝑢 ↔ 𝑣 𝑅 𝑚 ) )
4	3	notbid	⊢ ( 𝑢 = 𝑚 → ( ¬ 𝑣 𝑅 𝑢 ↔ ¬ 𝑣 𝑅 𝑚 ) )
5	4	ralbidv	⊢ ( 𝑢 = 𝑚 → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ↔ ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑚 ) )
6	5	cbvriotavw	⊢ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) = ( ℩ 𝑚 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑚 )
7		nfcv	⊢ Ⅎ 𝑥 𝐴
8		nfcv	⊢ Ⅎ 𝑙 𝐴
9		nfv	⊢ Ⅎ 𝑙 𝑤 ∈ 𝐵
10		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑙 / 𝑥 ⦌ 𝐵
11	10	nfcri	⊢ Ⅎ 𝑥 𝑤 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵
12		csbeq1a	⊢ ( 𝑥 = 𝑙 → 𝐵 = ⦋ 𝑙 / 𝑥 ⦌ 𝐵 )
13	12	eleq2d	⊢ ( 𝑥 = 𝑙 → ( 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
14	7 8 9 11 13	cbvrabw	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } = { 𝑙 ∈ 𝐴 ∣ 𝑤 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 }
15		eleq1w	⊢ ( 𝑤 = 𝑘 → ( 𝑤 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ↔ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
16	15	rabbidv	⊢ ( 𝑤 = 𝑘 → { 𝑙 ∈ 𝐴 ∣ 𝑤 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } = { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } )
17	14 16	eqtrid	⊢ ( 𝑤 = 𝑘 → { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } = { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } )
18		breq1	⊢ ( 𝑣 = 𝑛 → ( 𝑣 𝑅 𝑚 ↔ 𝑛 𝑅 𝑚 ) )
19	18	notbid	⊢ ( 𝑣 = 𝑛 → ( ¬ 𝑣 𝑅 𝑚 ↔ ¬ 𝑛 𝑅 𝑚 ) )
20	19	adantl	⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑛 ) → ( ¬ 𝑣 𝑅 𝑚 ↔ ¬ 𝑛 𝑅 𝑚 ) )
21	17	adantr	⊢ ( ( 𝑤 = 𝑘 ∧ 𝑣 = 𝑛 ) → { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } = { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } )
22	20 21	cbvraldva2	⊢ ( 𝑤 = 𝑘 → ( ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑚 ↔ ∀ 𝑛 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ¬ 𝑛 𝑅 𝑚 ) )
23	17 22	riotaeqbidv	⊢ ( 𝑤 = 𝑘 → ( ℩ 𝑚 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑚 ) = ( ℩ 𝑚 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ∀ 𝑛 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ¬ 𝑛 𝑅 𝑚 ) )
24	6 23	eqtrid	⊢ ( 𝑤 = 𝑘 → ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) = ( ℩ 𝑚 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ∀ 𝑛 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ¬ 𝑛 𝑅 𝑚 ) )
25	24	cbvmptv	⊢ ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) ) = ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑚 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ∀ 𝑛 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ¬ 𝑛 𝑅 𝑚 ) )
26		nfcv	⊢ Ⅎ 𝑙 𝐵
27	26 10 12	cbviun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵
28	27	mpteq1i	⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑚 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ∀ 𝑛 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ¬ 𝑛 𝑅 𝑚 ) ) = ( 𝑘 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ↦ ( ℩ 𝑚 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ∀ 𝑛 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ¬ 𝑛 𝑅 𝑚 ) )
29	1 25 28	3eqtri	⊢ 𝐹 = ( 𝑘 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ↦ ( ℩ 𝑚 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ∀ 𝑛 ∈ { 𝑙 ∈ 𝐴 ∣ 𝑘 ∈ ⦋ 𝑙 / 𝑥 ⦌ 𝐵 } ¬ 𝑛 𝑅 𝑚 ) )
30		simpl	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → 𝑦 = 𝑜 )
31	27	a1i	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 )
32	30 31	eleq12d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
33		simpr	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → 𝑧 = 𝑝 )
34	33 31	eleq12d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
35	32 34	anbi12d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ∧ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) ) )
36	30	fveq2d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑜 ) )
37	33	fveq2d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑝 ) )
38	36 37	breq12d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑜 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) )
39	36 37	eqeq12d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑜 ) = ( 𝐹 ‘ 𝑝 ) ) )
40	36	csbeq1d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝑆 )
41		csbcow	⊢ ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑙 ⦌ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑥 ⦌ 𝑆
42	40 41	eqtr4di	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑙 ⦌ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 )
43	30 42 33	breq123d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ↔ 𝑜 ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑙 ⦌ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 𝑝 ) )
44	39 43	anbi12d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑜 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑜 ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑙 ⦌ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 𝑝 ) ) )
45	38 44	orbi12d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑜 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑜 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑜 ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑙 ⦌ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 𝑝 ) ) ) )
46	35 45	anbi12d	⊢ ( ( 𝑦 = 𝑜 ∧ 𝑧 = 𝑝 ) → ( ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) ↔ ( ( 𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ∧ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑜 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑜 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑜 ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑙 ⦌ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 𝑝 ) ) ) ) )
47	46	cbvopabv	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) } = { ⟨ 𝑜 , 𝑝 ⟩ ∣ ( ( 𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ∧ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑜 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑜 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑜 ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑙 ⦌ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 𝑝 ) ) ) }
48	2 47	eqtri	⊢ 𝑇 = { ⟨ 𝑜 , 𝑝 ⟩ ∣ ( ( 𝑜 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ∧ 𝑝 ∈ ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑜 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑜 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑜 ⦋ ( 𝐹 ‘ 𝑜 ) / 𝑙 ⦌ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 𝑝 ) ) ) }
49		breq1	⊢ ( 𝑞 = 𝑡 → ( 𝑞 𝑅 𝑠 ↔ 𝑡 𝑅 𝑠 ) )
50	49	notbid	⊢ ( 𝑞 = 𝑡 → ( ¬ 𝑞 𝑅 𝑠 ↔ ¬ 𝑡 𝑅 𝑠 ) )
51	50	cbvralvw	⊢ ( ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑠 ↔ ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
52	51	a1i	⊢ ( 𝑠 ∈ ( 𝐹 “ 𝑟 ) → ( ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑠 ↔ ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 ) )
53	52	riotabiia	⊢ ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑠 ) = ( ℩ 𝑠 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑡 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑡 𝑅 𝑠 )
54	29 48 53	weiunfrlem2	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) → 𝑇 Fr ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 )
55		nfv	⊢ Ⅎ 𝑙 𝑆 Fr 𝐵
56		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑙 / 𝑥 ⦌ 𝑆
57	56 10	nffr	⊢ Ⅎ 𝑥 ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝑙 / 𝑥 ⦌ 𝐵
58		csbeq1a	⊢ ( 𝑥 = 𝑙 → 𝑆 = ⦋ 𝑙 / 𝑥 ⦌ 𝑆 )
59		freq1	⊢ ( 𝑆 = ⦋ 𝑙 / 𝑥 ⦌ 𝑆 → ( 𝑆 Fr 𝐵 ↔ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr 𝐵 ) )
60	58 59	syl	⊢ ( 𝑥 = 𝑙 → ( 𝑆 Fr 𝐵 ↔ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr 𝐵 ) )
61		freq2	⊢ ( 𝐵 = ⦋ 𝑙 / 𝑥 ⦌ 𝐵 → ( ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr 𝐵 ↔ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
62	12 61	syl	⊢ ( 𝑥 = 𝑙 → ( ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr 𝐵 ↔ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
63	60 62	bitrd	⊢ ( 𝑥 = 𝑙 → ( 𝑆 Fr 𝐵 ↔ ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
64	55 57 63	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ↔ ∀ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝑙 / 𝑥 ⦌ 𝐵 )
65	64	3anbi3i	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) ↔ ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝑆 Fr ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
66		freq2	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 → ( 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑇 Fr ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 ) )
67	27 66	ax-mp	⊢ ( 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑇 Fr ∪ 𝑙 ∈ 𝐴 ⦋ 𝑙 / 𝑥 ⦌ 𝐵 )
68	54 65 67	3imtr4i	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝑆 Fr 𝐵 ) → 𝑇 Fr ∪ 𝑥 ∈ 𝐴 𝐵 )