Metamath Proof Explorer

Theorem weiunfrlem

Description: Lemma for weiunfr . (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 )
weiunfrlem.5 
|- E = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p )
weiunfrlem.6 
|- ( ph -> r C_ U_ x e. A B )
weiunfrlem.7 
|- ( ph -> r =/= (/) )
Assertion weiunfrlem 
|- ( ph -> ( E e. ( F " r ) /\ A. t e. r -. ( F ` t ) R E /\ A. t e. ( r i^i [_ E / x ]_ B ) ( F ` t ) = E ) )

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 weiunfrlem.5 
 |-  E = ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p )
6 weiunfrlem.6 
 |-  ( ph -> r C_ U_ x e. A B )
7 weiunfrlem.7 
 |-  ( ph -> r =/= (/) )
8 1 2 3 4 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 ) ) )
9 8 simp1d 
 |-  ( ph -> F : U_ x e. A B --> A )
10 9 fimassd 
 |-  ( ph -> ( F " r ) C_ A )
11 9 fdmd 
 |-  ( ph -> dom F = U_ x e. A B )
12 6 11 sseqtrrd 
 |-  ( ph -> r C_ dom F )
13 sseqin2 
 |-  ( r C_ dom F <-> ( dom F i^i r ) = r )
14 12 13 sylib 
 |-  ( ph -> ( dom F i^i r ) = r )
15 14 7 eqnetrd 
 |-  ( ph -> ( dom F i^i r ) =/= (/) )
16 15 imadisjlnd 
 |-  ( ph -> ( F " r ) =/= (/) )
17 wereu2 
 |-  ( ( ( R We A /\ R Se A ) /\ ( ( F " r ) C_ A /\ ( F " r ) =/= (/) ) ) -> E! p e. ( F " r ) A. q e. ( F " r ) -. q R p )
18 3 4 10 16 17 syl22anc 
 |-  ( ph -> E! p e. ( F " r ) A. q e. ( F " r ) -. q R p )
19 riotacl2 
 |-  ( E! p e. ( F " r ) A. q e. ( F " r ) -. q R p -> ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. { p e. ( F " r ) | A. q e. ( F " r ) -. q R p } )
20 18 19 syl 
 |-  ( ph -> ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) e. { p e. ( F " r ) | A. q e. ( F " r ) -. q R p } )
21 simpr 
 |-  ( ( n = p /\ o = q ) -> o = q )
22 simpl 
 |-  ( ( n = p /\ o = q ) -> n = p )
23 21 22 breq12d 
 |-  ( ( n = p /\ o = q ) -> ( o R n <-> q R p ) )
24 23 notbid 
 |-  ( ( n = p /\ o = q ) -> ( -. o R n <-> -. q R p ) )
25 24 cbvraldva 
 |-  ( n = p -> ( A. o e. ( F " r ) -. o R n <-> A. q e. ( F " r ) -. q R p ) )
26 25 cbvrabv 
 |-  { n e. ( F " r ) | A. o e. ( F " r ) -. o R n } = { p e. ( F " r ) | A. q e. ( F " r ) -. q R p }
27 20 5 26 3eltr4g 
 |-  ( ph -> E e. { n e. ( F " r ) | A. o e. ( F " r ) -. o R n } )
28 breq2 
 |-  ( n = E -> ( o R n <-> o R E ) )
29 28 notbid 
 |-  ( n = E -> ( -. o R n <-> -. o R E ) )
30 29 ralbidv 
 |-  ( n = E -> ( A. o e. ( F " r ) -. o R n <-> A. o e. ( F " r ) -. o R E ) )
31 30 elrab 
 |-  ( E e. { n e. ( F " r ) | A. o e. ( F " r ) -. o R n } <-> ( E e. ( F " r ) /\ A. o e. ( F " r ) -. o R E ) )
32 27 31 sylib 
 |-  ( ph -> ( E e. ( F " r ) /\ A. o e. ( F " r ) -. o R E ) )
33 32 simpld 
 |-  ( ph -> E e. ( F " r ) )
34 32 simprd 
 |-  ( ph -> A. o e. ( F " r ) -. o R E )
35 9 ffnd 
 |-  ( ph -> F Fn U_ x e. A B )
36 breq1 
 |-  ( o = ( F ` t ) -> ( o R E <-> ( F ` t ) R E ) )
37 36 notbid 
 |-  ( o = ( F ` t ) -> ( -. o R E <-> -. ( F ` t ) R E ) )
38 37 ralima 
 |-  ( ( F Fn U_ x e. A B /\ r C_ U_ x e. A B ) -> ( A. o e. ( F " r ) -. o R E <-> A. t e. r -. ( F ` t ) R E ) )
39 35 6 38 syl2anc 
 |-  ( ph -> ( A. o e. ( F " r ) -. o R E <-> A. t e. r -. ( F ` t ) R E ) )
40 34 39 mpbid 
 |-  ( ph -> A. t e. r -. ( F ` t ) R E )
41 simpr 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> t e. ( r i^i [_ E / x ]_ B ) )
42 41 elin1d 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> t e. r )
43 rspa 
 |-  ( ( A. t e. r -. ( F ` t ) R E /\ t e. r ) -> -. ( F ` t ) R E )
44 40 42 43 syl2an2r 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> -. ( F ` t ) R E )
45 csbeq1 
 |-  ( s = E -> [_ s / x ]_ B = [_ E / x ]_ B )
46 breq1 
 |-  ( s = E -> ( s R ( F ` t ) <-> E R ( F ` t ) ) )
47 46 notbid 
 |-  ( s = E -> ( -. s R ( F ` t ) <-> -. E R ( F ` t ) ) )
48 45 47 raleqbidv 
 |-  ( s = E -> ( A. t e. [_ s / x ]_ B -. s R ( F ` t ) <-> A. t e. [_ E / x ]_ B -. E R ( F ` t ) ) )
49 8 simp3d 
 |-  ( ph -> A. s e. A A. t e. [_ s / x ]_ B -. s R ( F ` t ) )
50 10 33 sseldd 
 |-  ( ph -> E e. A )
51 48 49 50 rspcdva 
 |-  ( ph -> A. t e. [_ E / x ]_ B -. E R ( F ` t ) )
52 41 elin2d 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> t e. [_ E / x ]_ B )
53 rspa 
 |-  ( ( A. t e. [_ E / x ]_ B -. E R ( F ` t ) /\ t e. [_ E / x ]_ B ) -> -. E R ( F ` t ) )
54 51 52 53 syl2an2r 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> -. E R ( F ` t ) )
55 weso 
 |-  ( R We A -> R Or A )
56 3 55 syl 
 |-  ( ph -> R Or A )
57 56 adantr 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> R Or A )
58 9 adantr 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> F : U_ x e. A B --> A )
59 6 adantr 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> r C_ U_ x e. A B )
60 59 42 sseldd 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> t e. U_ x e. A B )
61 58 60 ffvelcdmd 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> ( F ` t ) e. A )
62 50 adantr 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> E e. A )
63 sotrieq2 
 |-  ( ( R Or A /\ ( ( F ` t ) e. A /\ E e. A ) ) -> ( ( F ` t ) = E <-> ( -. ( F ` t ) R E /\ -. E R ( F ` t ) ) ) )
64 57 61 62 63 syl12anc 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> ( ( F ` t ) = E <-> ( -. ( F ` t ) R E /\ -. E R ( F ` t ) ) ) )
65 44 54 64 mpbir2and 
 |-  ( ( ph /\ t e. ( r i^i [_ E / x ]_ B ) ) -> ( F ` t ) = E )
66 65 ralrimiva 
 |-  ( ph -> A. t e. ( r i^i [_ E / x ]_ B ) ( F ` t ) = E )
67 33 40 66 3jca 
 |-  ( ph -> ( E e. ( F " r ) /\ A. t e. r -. ( F ` t ) R E /\ A. t e. ( r i^i [_ E / x ]_ B ) ( F ` t ) = E ) )