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 
|- 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 ) )
weiunse.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 weiunse.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 weiunse.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 weiunlem2 
 |-  ( ( R We A /\ R Se A ) -> ( F : U_ x e. A B --> A /\ A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B /\ A. t e. U_ x e. A B A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) ) )
6 4 3 5 syl2anc 
 |-  ( ( ( 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. t e. U_ x e. A B A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) ) )
7 6 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 )
8 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 )
9 7 8 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 )
10 seex 
 |-  ( ( R Se A /\ ( F ` p ) e. A ) -> { r e. A | r R ( F ` p ) } e. _V )
11 3 9 10 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 )
12 snex 
 |-  { ( F ` p ) } e. _V
13 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 )
14 11 12 13 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 )
15 ssrab2 
 |-  { r e. A | r R ( F ` p ) } C_ A
16 15 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 )
17 9 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 )
18 16 17 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 )
19 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 )
20 elex 
 |-  ( B e. V -> B e. _V )
21 20 ralimi 
 |-  ( A. x e. A B e. V -> A. x e. A B e. _V )
22 19 21 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 )
23 nfv 
 |-  F/ s B e. _V
24 nfcsb1v 
 |-  F/_ x [_ s / x ]_ B
25 24 nfel1 
 |-  F/ x [_ s / x ]_ B e. _V
26 csbeq1a 
 |-  ( x = s -> B = [_ s / x ]_ B )
27 26 eleq1d 
 |-  ( x = s -> ( B e. _V <-> [_ s / x ]_ B e. _V ) )
28 23 25 27 cbvralw 
 |-  ( A. x e. A B e. _V <-> A. s e. A [_ s / x ]_ B e. _V )
29 22 28 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 )
30 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 ) )
31 18 29 30 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 )
32 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 )
33 14 31 32 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 )
34 7 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 )
35 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 )
36 34 35 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 )
37 breq1 
 |-  ( r = ( F ` q ) -> ( r R ( F ` p ) <-> ( F ` q ) R ( F ` p ) ) )
38 37 elrab 
 |-  ( ( F ` q ) e. { r e. A | r R ( F ` p ) } <-> ( ( F ` q ) e. A /\ ( F ` q ) R ( F ` p ) ) )
39 elun1 
 |-  ( ( F ` q ) e. { r e. A | r R ( F ` p ) } -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
40 38 39 sylbir 
 |-  ( ( ( F ` q ) e. A /\ ( F ` q ) R ( F ` p ) ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
41 36 40 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 ) } ) )
42 fvex 
 |-  ( F ` q ) e. _V
43 42 elsn 
 |-  ( ( F ` q ) e. { ( F ` p ) } <-> ( F ` q ) = ( F ` p ) )
44 elun2 
 |-  ( ( F ` q ) e. { ( F ` p ) } -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
45 43 44 sylbir 
 |-  ( ( F ` q ) = ( F ` p ) -> ( F ` q ) e. ( { r e. A | r R ( F ` p ) } u. { ( F ` p ) } ) )
46 45 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 ) } ) )
47 simpl 
 |-  ( ( y = q /\ z = p ) -> y = q )
48 47 fveq2d 
 |-  ( ( y = q /\ z = p ) -> ( F ` y ) = ( F ` q ) )
49 simpr 
 |-  ( ( y = q /\ z = p ) -> z = p )
50 49 fveq2d 
 |-  ( ( y = q /\ z = p ) -> ( F ` z ) = ( F ` p ) )
51 48 50 breq12d 
 |-  ( ( y = q /\ z = p ) -> ( ( F ` y ) R ( F ` z ) <-> ( F ` q ) R ( F ` p ) ) )
52 48 50 eqeq12d 
 |-  ( ( y = q /\ z = p ) -> ( ( F ` y ) = ( F ` z ) <-> ( F ` q ) = ( F ` p ) ) )
53 48 csbeq1d 
 |-  ( ( y = q /\ z = p ) -> [_ ( F ` y ) / x ]_ S = [_ ( F ` q ) / x ]_ S )
54 47 53 49 breq123d 
 |-  ( ( y = q /\ z = p ) -> ( y [_ ( F ` y ) / x ]_ S z <-> q [_ ( F ` q ) / x ]_ S p ) )
55 52 54 anbi12d 
 |-  ( ( y = q /\ z = p ) -> ( ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) <-> ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) )
56 51 55 orbi12d 
 |-  ( ( y = q /\ z = p ) -> ( ( ( F ` y ) R ( F ` z ) \/ ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) <-> ( ( F ` q ) R ( F ` p ) \/ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) ) )
57 56 2 brab2a 
 |-  ( 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 ) ) ) )
58 57 simprbi 
 |-  ( q T p -> ( ( F ` q ) R ( F ` p ) \/ ( ( F ` q ) = ( F ` p ) /\ q [_ ( F ` q ) / x ]_ S p ) ) )
59 58 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 ) ) )
60 41 46 59 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 ) } ) )
61 id 
 |-  ( t = q -> t = q )
62 fveq2 
 |-  ( t = q -> ( F ` t ) = ( F ` q ) )
63 62 csbeq1d 
 |-  ( t = q -> [_ ( F ` t ) / x ]_ B = [_ ( F ` q ) / x ]_ B )
64 61 63 eleq12d 
 |-  ( t = q -> ( t e. [_ ( F ` t ) / x ]_ B <-> q e. [_ ( F ` q ) / x ]_ B ) )
65 6 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 )
66 65 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 )
67 64 66 35 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 )
68 csbeq1 
 |-  ( s = ( F ` q ) -> [_ s / x ]_ B = [_ ( F ` q ) / x ]_ B )
69 68 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 )
70 60 67 69 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 )
71 70 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 )
72 33 71 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 )
73 72 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 )
74 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 )
75 73 74 sylibr 
 |-  ( ( R We A /\ R Se A /\ A. x e. A B e. V ) -> T Se U_ x e. A B )