Theorem weiunse

Description: The relation constructed in weiunpo , weiunso , weiunfr , and weiunwe is set-like if all members of the indexed union are sets. (Contributed by Matthew House, 23-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		weiun.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2		weiun.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
3		simpl2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑅 Se 𝐴 )
4		simpl1	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑅 We 𝐴 )
5	1 2 4 3	weiunlem2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑠 ∈ 𝐴 ∀ 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) )
6	5	simp1d	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
7		simpr	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
8	6 7	ffvelcdmd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 )
9		seex	⊢ ( ( 𝑅 Se 𝐴 ∧ ( 𝐹 ‘ 𝑝 ) ∈ 𝐴 ) → { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∈ V )
10	3 8 9	syl2anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∈ V )
11		snex	⊢ { ( 𝐹 ‘ 𝑝 ) } ∈ V
12		unexg	⊢ ( ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∈ V ∧ { ( 𝐹 ‘ 𝑝 ) } ∈ V ) → ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ∈ V )
13	10 11 12	sylancl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ∈ V )
14		ssrab2	⊢ { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ⊆ 𝐴
15	14	a1i	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ⊆ 𝐴 )
16	8	snssd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { ( 𝐹 ‘ 𝑝 ) } ⊆ 𝐴 )
17	15 16	unssd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⊆ 𝐴 )
18		simpl3	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
19		elex	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
20	19	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
21	18 20	syl	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
22		nfv	⊢ Ⅎ 𝑠 𝐵 ∈ V
23		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐵
24	23	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V
25		csbeq1a	⊢ ( 𝑥 = 𝑠 → 𝐵 = ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
26	25	eleq1d	⊢ ( 𝑥 = 𝑠 → ( 𝐵 ∈ V ↔ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) )
27	22 24 26	cbvralw	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V )
28	21 27	sylib	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V )
29		ssralv	⊢ ( ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⊆ 𝐴 → ( ∀ 𝑠 ∈ 𝐴 ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V → ∀ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) )
30	17 28 29	sylc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V )
31		iunexg	⊢ ( ( ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ∈ V ∧ ∀ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V ) → ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V )
32	13 30 31	syl2anc	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ∈ V )
33	6	3ad2ant1	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
34		simp2	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
35	33 34	ffvelcdmd	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
36		breq1	⊢ ( 𝑟 = ( 𝐹 ‘ 𝑞 ) → ( 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) )
37	36	elrab	⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ↔ ( ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) )
38		elun1	⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) )
39	37 38	sylbir	⊢ ( ( ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) )
40	35 39	sylan	⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) )
41		fvex	⊢ ( 𝐹 ‘ 𝑞 ) ∈ V
42	41	elsn	⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ { ( 𝐹 ‘ 𝑝 ) } ↔ ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) )
43		elun2	⊢ ( ( 𝐹 ‘ 𝑞 ) ∈ { ( 𝐹 ‘ 𝑝 ) } → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) )
44	42 43	sylbir	⊢ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) )
45	44	ad2antrl	⊢ ( ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) ∧ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) )
46	1 2	weiunlem1	⊢ ( 𝑞 𝑇 𝑝 ↔ ( ( 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) ) )
47	46	simprbi	⊢ ( 𝑞 𝑇 𝑝 → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
48	47	3ad2ant3	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ∨ ( ( 𝐹 ‘ 𝑞 ) = ( 𝐹 ‘ 𝑝 ) ∧ 𝑞 ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝑆 𝑝 ) ) )
49	40 45 48	mpjaodan	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) )
50		id	⊢ ( 𝑡 = 𝑞 → 𝑡 = 𝑞 )
51		fveq2	⊢ ( 𝑡 = 𝑞 → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ 𝑞 ) )
52	51	csbeq1d	⊢ ( 𝑡 = 𝑞 → ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
53	50 52	eleq12d	⊢ ( 𝑡 = 𝑞 → ( 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ↔ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) )
54	5	simp2d	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
55	54	3ad2ant1	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 )
56	53 55 34	rspcdva	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
57		csbeq1	⊢ ( 𝑠 = ( 𝐹 ‘ 𝑞 ) → ⦋ 𝑠 / 𝑥 ⦌ 𝐵 = ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 )
58	57	eliuni	⊢ ( ( ( 𝐹 ‘ 𝑞 ) ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ∧ 𝑞 ∈ ⦋ ( 𝐹 ‘ 𝑞 ) / 𝑥 ⦌ 𝐵 ) → 𝑞 ∈ ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
59	49 56 58	syl2anc	⊢ ( ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑞 𝑇 𝑝 ) → 𝑞 ∈ ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
60	59	rabssdv	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∣ 𝑞 𝑇 𝑝 } ⊆ ∪ 𝑠 ∈ ( { 𝑟 ∈ 𝐴 ∣ 𝑟 𝑅 ( 𝐹 ‘ 𝑝 ) } ∪ { ( 𝐹 ‘ 𝑝 ) } ) ⦋ 𝑠 / 𝑥 ⦌ 𝐵 )
61	32 60	ssexd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) ∧ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → { 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∣ 𝑞 𝑇 𝑝 } ∈ V )
62	61	ralrimiva	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ∀ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 { 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∣ 𝑞 𝑇 𝑝 } ∈ V )
63		df-se	⊢ ( 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑝 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 { 𝑞 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∣ 𝑞 𝑇 𝑝 } ∈ V )
64	62 63	sylibr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵 )