Metamath Proof Explorer

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 weiunse.1 ⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
weiunse.2 ⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
Assertion weiunse ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → 𝑇 Se ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

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