Metamath Proof Explorer

Theorem weiunlem2

Description: Lemma for weiunpo , weiunso , weiunfr , and weiunse . (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 ) ) ) }
weiunlem2.3 
|- ( ph -> R We A )
weiunlem2.4 
|- ( ph -> R Se A )
Assertion weiunlem2 
|- ( ph -> ( 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 ) ) )

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 weiunlem2.3 
 |-  ( ph -> R We A )
4 weiunlem2.4 
 |-  ( ph -> R Se A )
5 riotaex 
 |-  ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) e. _V
6 5 1 fnmpti 
 |-  F Fn U_ x e. A B
7 6 a1i 
 |-  ( ( R We A /\ R Se A ) -> F Fn U_ x e. A B )
8 breq2 
 |-  ( u = r -> ( v R u <-> v R r ) )
9 8 notbid 
 |-  ( u = r -> ( -. v R u <-> -. v R r ) )
10 9 ralbidv 
 |-  ( u = r -> ( A. v e. { x e. A | w e. B } -. v R u <-> A. v e. { x e. A | w e. B } -. v R r ) )
11 10 cbvriotavw 
 |-  ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) = ( iota_ r e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R r )
12 eleq1w 
 |-  ( w = t -> ( w e. B <-> t e. B ) )
13 12 rabbidv 
 |-  ( w = t -> { x e. A | w e. B } = { x e. A | t e. B } )
14 breq1 
 |-  ( v = s -> ( v R r <-> s R r ) )
15 14 notbid 
 |-  ( v = s -> ( -. v R r <-> -. s R r ) )
16 15 cbvralvw 
 |-  ( A. v e. { x e. A | w e. B } -. v R r <-> A. s e. { x e. A | w e. B } -. s R r )
17 13 raleqdv 
 |-  ( w = t -> ( A. s e. { x e. A | w e. B } -. s R r <-> A. s e. { x e. A | t e. B } -. s R r ) )
18 16 17 bitrid 
 |-  ( w = t -> ( A. v e. { x e. A | w e. B } -. v R r <-> A. s e. { x e. A | t e. B } -. s R r ) )
19 13 18 riotaeqbidv 
 |-  ( w = t -> ( iota_ r e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R r ) = ( iota_ r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r ) )
20 11 19 eqtrid 
 |-  ( w = t -> ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) = ( iota_ r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r ) )
21 20 1 5 fvmpt3i 
 |-  ( t e. U_ x e. A B -> ( F ` t ) = ( iota_ r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r ) )
22 21 adantl 
 |-  ( ( ( R We A /\ R Se A ) /\ t e. U_ x e. A B ) -> ( F ` t ) = ( iota_ r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r ) )
23 eliun 
 |-  ( t e. U_ x e. A B <-> E. x e. A t e. B )
24 rabn0 
 |-  ( { x e. A | t e. B } =/= (/) <-> E. x e. A t e. B )
25 23 24 bitr4i 
 |-  ( t e. U_ x e. A B <-> { x e. A | t e. B } =/= (/) )
26 ssrab2 
 |-  { x e. A | t e. B } C_ A
27 wereu2 
 |-  ( ( ( R We A /\ R Se A ) /\ ( { x e. A | t e. B } C_ A /\ { x e. A | t e. B } =/= (/) ) ) -> E! r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r )
28 26 27 mpanr1 
 |-  ( ( ( R We A /\ R Se A ) /\ { x e. A | t e. B } =/= (/) ) -> E! r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r )
29 25 28 sylan2b 
 |-  ( ( ( R We A /\ R Se A ) /\ t e. U_ x e. A B ) -> E! r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r )
30 riotacl2 
 |-  ( E! r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r -> ( iota_ r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r ) e. { r e. { x e. A | t e. B } | A. s e. { x e. A | t e. B } -. s R r } )
31 29 30 syl 
 |-  ( ( ( R We A /\ R Se A ) /\ t e. U_ x e. A B ) -> ( iota_ r e. { x e. A | t e. B } A. s e. { x e. A | t e. B } -. s R r ) e. { r e. { x e. A | t e. B } | A. s e. { x e. A | t e. B } -. s R r } )
32 22 31 eqeltrd 
 |-  ( ( ( R We A /\ R Se A ) /\ t e. U_ x e. A B ) -> ( F ` t ) e. { r e. { x e. A | t e. B } | A. s e. { x e. A | t e. B } -. s R r } )
33 elrabi 
 |-  ( ( F ` t ) e. { r e. { x e. A | t e. B } | A. s e. { x e. A | t e. B } -. s R r } -> ( F ` t ) e. { x e. A | t e. B } )
34 elrabi 
 |-  ( ( F ` t ) e. { x e. A | t e. B } -> ( F ` t ) e. A )
35 32 33 34 3syl 
 |-  ( ( ( R We A /\ R Se A ) /\ t e. U_ x e. A B ) -> ( F ` t ) e. A )
36 35 ralrimiva 
 |-  ( ( R We A /\ R Se A ) -> A. t e. U_ x e. A B ( F ` t ) e. A )
37 ffnfv 
 |-  ( F : U_ x e. A B --> A <-> ( F Fn U_ x e. A B /\ A. t e. U_ x e. A B ( F ` t ) e. A ) )
38 7 36 37 sylanbrc 
 |-  ( ( R We A /\ R Se A ) -> F : U_ x e. A B --> A )
39 dfsbcq 
 |-  ( s = ( F ` t ) -> ( [. s / x ]. t e. B <-> [. ( F ` t ) / x ]. t e. B ) )
40 nfcv 
 |-  F/_ x A
41 40 elrabsf 
 |-  ( s e. { x e. A | t e. B } <-> ( s e. A /\ [. s / x ]. t e. B ) )
42 41 simprbi 
 |-  ( s e. { x e. A | t e. B } -> [. s / x ]. t e. B )
43 39 42 vtoclga 
 |-  ( ( F ` t ) e. { x e. A | t e. B } -> [. ( F ` t ) / x ]. t e. B )
44 32 33 43 3syl 
 |-  ( ( ( R We A /\ R Se A ) /\ t e. U_ x e. A B ) -> [. ( F ` t ) / x ]. t e. B )
45 sbcel2 
 |-  ( [. ( F ` t ) / x ]. t e. B <-> t e. [_ ( F ` t ) / x ]_ B )
46 44 45 sylib 
 |-  ( ( ( R We A /\ R Se A ) /\ t e. U_ x e. A B ) -> t e. [_ ( F ` t ) / x ]_ B )
47 46 ralrimiva 
 |-  ( ( R We A /\ R Se A ) -> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B )
48 simpr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( s e. A /\ t e. [_ s / x ]_ B ) ) -> ( s e. A /\ t e. [_ s / x ]_ B ) )
49 sbcel2 
 |-  ( [. s / x ]. t e. B <-> t e. [_ s / x ]_ B )
50 49 anbi2i 
 |-  ( ( s e. A /\ [. s / x ]. t e. B ) <-> ( s e. A /\ t e. [_ s / x ]_ B ) )
51 41 50 bitri 
 |-  ( s e. { x e. A | t e. B } <-> ( s e. A /\ t e. [_ s / x ]_ B ) )
52 48 51 sylibr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( s e. A /\ t e. [_ s / x ]_ B ) ) -> s e. { x e. A | t e. B } )
53 52 ne0d 
 |-  ( ( ( R We A /\ R Se A ) /\ ( s e. A /\ t e. [_ s / x ]_ B ) ) -> { x e. A | t e. B } =/= (/) )
54 53 25 sylibr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( s e. A /\ t e. [_ s / x ]_ B ) ) -> t e. U_ x e. A B )
55 breq2 
 |-  ( r = ( F ` t ) -> ( s R r <-> s R ( F ` t ) ) )
56 55 notbid 
 |-  ( r = ( F ` t ) -> ( -. s R r <-> -. s R ( F ` t ) ) )
57 56 ralbidv 
 |-  ( r = ( F ` t ) -> ( A. s e. { x e. A | t e. B } -. s R r <-> A. s e. { x e. A | t e. B } -. s R ( F ` t ) ) )
58 57 elrab 
 |-  ( ( F ` t ) e. { r e. { x e. A | t e. B } | A. s e. { x e. A | t e. B } -. s R r } <-> ( ( F ` t ) e. { x e. A | t e. B } /\ A. s e. { x e. A | t e. B } -. s R ( F ` t ) ) )
59 58 simprbi 
 |-  ( ( F ` t ) e. { r e. { x e. A | t e. B } | A. s e. { x e. A | t e. B } -. s R r } -> A. s e. { x e. A | t e. B } -. s R ( F ` t ) )
60 32 59 syl 
 |-  ( ( ( R We A /\ R Se A ) /\ t e. U_ x e. A B ) -> A. s e. { x e. A | t e. B } -. s R ( F ` t ) )
61 54 60 syldan 
 |-  ( ( ( R We A /\ R Se A ) /\ ( s e. A /\ t e. [_ s / x ]_ B ) ) -> A. s e. { x e. A | t e. B } -. s R ( F ` t ) )
62 rsp 
 |-  ( A. s e. { x e. A | t e. B } -. s R ( F ` t ) -> ( s e. { x e. A | t e. B } -> -. s R ( F ` t ) ) )
63 61 52 62 sylc 
 |-  ( ( ( R We A /\ R Se A ) /\ ( s e. A /\ t e. [_ s / x ]_ B ) ) -> -. s R ( F ` t ) )
64 63 ralrimivva 
 |-  ( ( R We A /\ R Se A ) -> A. s e. A A. t e. [_ s / x ]_ B -. s R ( F ` t ) )
65 38 47 64 3jca 
 |-  ( ( 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. s e. A A. t e. [_ s / x ]_ B -. s R ( F ` t ) ) )
66 3 4 65 syl2anc 
 |-  ( ph -> ( 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 ) ) )