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 weiun.1 
|- F = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
weiun.2 
|- T = { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) }
Assertion weiunse 
|- ( ( R We A /\ R Se A /\ A. x e. A B e. V ) -> T Se U_ x e. A B )

Proof

Step Hyp Ref Expression
1 weiun.1 
 |-  F = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) )
2 weiun.2 
 |-  T = { <. y , z >. | ( ( y e. U_ x e. A B /\ z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) }
3 simpl2 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> R Se A )
4 simpl1 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> R We A )
5 1 2 4 3 weiunlem2 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> ( F : U_ x e. A B --> A /\ A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B /\ A. s e. A A. t e. [_ s / x ]_ B -. s R ( F ` t ) ) )
6 5 simp1d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> F : U_ x e. A B --> A )
7 simpr 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> p e. U_ x e. A B )
8 6 7 ffvelcdmd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> ( F ` p ) e. A )
9 seex 
 |-  ( ( R Se A /\ ( F ` p ) e. A ) -> { r e. A | r R ( F ` p ) } e. _V )
10 3 8 9 syl2anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { r e. A | r R ( F ` p ) } e. _V )
11 snex 
 |-  { ( F ` p ) } e. _V
12 unexg 
 |-  ( ( { r e. A | r R ( F ` p ) } e. _V /\ { ( F ` p ) } e. _V ) -> ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) e. _V )
13 10 11 12 sylancl 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) e. _V )
14 ssrab2 
 |-  { r e. A | r R ( F ` p ) } C_ A
15 14 a1i 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { r e. A | r R ( F ` p ) } C_ A )
16 8 snssd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { ( F ` p ) } C_ A )
17 15 16 unssd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) C_ A )
18 simpl3 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. x e. A B e. V )
19 elex 
 |-  ( B e. V -> B e. _V )
20 19 ralimi 
 |-  ( A. x e. A B e. V -> A. x e. A B e. _V )
21 18 20 syl 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. x e. A B e. _V )
22 nfv 
 |-  F/ s B e. _V
23 nfcsb1v 
 |-  F/_ x [_ s / x ]_ B
24 23 nfel1 
 |-  F/ x [_ s / x ]_ B e. _V
25 csbeq1a 
 |-  ( x = s -> B = [_ s / x ]_ B )
26 25 eleq1d 
 |-  ( x = s -> ( B e. _V <-> [_ s / x ]_ B e. _V ) )
27 22 24 26 cbvralw 
 |-  ( A. x e. A B e. _V <-> A. s e. A [_ s / x ]_ B e. _V )
28 21 27 sylib 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. s e. A [_ s / x ]_ B e. _V )
29 ssralv 
 |-  ( ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) C_ A -> ( A. s e. A [_ s / x ]_ B e. _V -> A. s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V ) )
30 17 28 29 sylc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V )
31 iunexg 
 |-  ( ( ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) e. _V /\ A. s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V ) -> U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V )
32 13 30 31 syl2anc 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B e. _V )
33 6 3ad2ant1 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> F : U_ x e. A B --> A )
34 simp2 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> q e. U_ x e. A B )
35 33 34 ffvelcdmd 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> ( F ` q ) e. A )
36 breq1 
 |-  ( r = ( F ` q ) -> ( r R ( F ` p ) <-> ( F ` q ) R ( F ` p ) ) )
37 36 elrab 
 |-  ( ( F ` q ) e. { r e. A | r R ( F ` p ) } <-> ( ( F ` q ) e. A /\ ( F ` q ) R ( F ` p ) ) )
38 elun1 
 |-  ( ( F ` q ) e. { r e. A | r R ( F ` p ) } -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
39 37 38 sylbir 
 |-  ( ( ( F ` q ) e. A /\ ( F ` q ) R ( F ` p ) ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
40 35 39 sylan 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) /\ ( F ` q ) R ( F ` p ) ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
41 fvex 
 |-  ( F ` q ) e. _V
42 41 elsn 
 |-  ( ( F ` q ) e. { ( F ` p ) } <-> ( F ` q ) = ( F ` p ) )
43 elun2 
 |-  ( ( F ` q ) e. { ( F ` p ) } -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
44 42 43 sylbir 
 |-  ( ( F ` q ) = ( F ` p ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
45 44 ad2antrl 
 |-  ( ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) /\ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
46 1 2 weiunlem1 
 |-  ( q T p <-> ( ( q e. U_ x e. A B /\ p e. U_ x e. A B ) /\ ( ( F ` q ) R ( F ` p ) \/ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) ) )
47 46 simprbi 
 |-  ( q T p -> ( ( F ` q ) R ( F ` p ) \/ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) )
48 47 3ad2ant3 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> ( ( F ` q ) R ( F ` p ) \/ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) )
49 40 45 48 mpjaodan 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
50 id 
 |-  ( t = q -> t = q )
51 fveq2 
 |-  ( t = q -> ( F ` t ) = ( F ` q ) )
52 51 csbeq1d 
 |-  ( t = q -> [_ ( F ` t ) / x ]_ B = [_ ( F ` q ) / x ]_ B )
53 50 52 eleq12d 
 |-  ( t = q -> ( t e. [_ ( F ` t ) / x ]_ B <-> q e. [_ ( F ` q ) / x ]_ B ) )
54 5 simp2d 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B )
55 54 3ad2ant1 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B )
56 53 55 34 rspcdva 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> q e. [_ ( F ` q ) / x ]_ B )
57 csbeq1 
 |-  ( s = ( F ` q ) -> [_ s / x ]_ B = [_ ( F ` q ) / x ]_ B )
58 57 eliuni 
 |-  ( ( ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) /\ q e. [_ ( F ` q ) / x ]_ B ) -> q e. U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B )
59 49 56 58 syl2anc 
 |-  ( ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) /\ q e. U_ x e. A B /\ q T p ) -> q e. U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B )
60 59 rabssdv 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { q e. U_ x e. A B | q T p } C_ U_ s e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) [_ s / x ]_ B )
61 32 60 ssexd 
 |-  ( ( ( R We A /\ R Se A /\ A. x e. A B e. V ) /\ p e. U_ x e. A B ) -> { q e. U_ x e. A B | q T p } e. _V )
62 61 ralrimiva 
 |-  ( ( R We A /\ R Se A /\ A. x e. A B e. V ) -> A. p e. U_ x e. A B { q e. U_ x e. A B | q T p } e. _V )
63 df-se 
 |-  ( T Se U_ x e. A B <-> A. p e. U_ x e. A B { q e. U_ x e. A B | q T p } e. _V )
64 62 63 sylibr 
 |-  ( ( R We A /\ R Se A /\ A. x e. A B e. V ) -> T Se U_ x e. A B )