Metamath Proof Explorer

Theorem weiunfrlem1

Description: Lemma for weiunfr . (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Hypotheses weiunfrlem1.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 ) )
weiunfrlem1.2 
|- C = ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s )
Assertion weiunfrlem1 
|- ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( C e. ( F " r ) /\ A. w e. r -. ( F ` w ) R C ) )

Proof

Step Hyp Ref Expression
1 weiunfrlem1.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 weiunfrlem1.2 
 |-  C = ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s )
3 simpl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( R We A /\ R Se A ) )
4 1 weiunlem1 
 |-  ( ( R We A /\ R Se A ) -> ( F : U_ x e. A B --> A /\ A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )
5 4 adantr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( F : U_ x e. A B --> A /\ A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) )
6 5 simp1d 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> F : U_ x e. A B --> A )
7 6 fimassd 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( F " r ) C_ A )
8 simprl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> r C_ U_ x e. A B )
9 6 fdmd 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> dom F = U_ x e. A B )
10 8 9 sseqtrrd 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> r C_ dom F )
11 sseqin2 
 |-  ( r C_ dom F <-> ( dom F i^i r ) = r )
12 10 11 sylib 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( dom F i^i r ) = r )
13 simprr 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> r =/= (/) )
14 12 13 eqnetrd 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( dom F i^i r ) =/= (/) )
15 14 imadisjlnd 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( F " r ) =/= (/) )
16 wereu2 
 |-  ( ( ( R We A /\ R Se A ) /\ ( ( F " r ) C_ A /\ ( F " r ) =/= (/) ) ) -> E! s e. ( F " r ) A. t e. ( F " r ) -. t R s )
17 3 7 15 16 syl12anc 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> E! s e. ( F " r ) A. t e. ( F " r ) -. t R s )
18 riotacl2 
 |-  ( E! s e. ( F " r ) A. t e. ( F " r ) -. t R s -> ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s ) e. { s e. ( F " r ) | A. t e. ( F " r ) -. t R s } )
19 17 18 syl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s ) e. { s e. ( F " r ) | A. t e. ( F " r ) -. t R s } )
20 2 19 eqeltrid 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> C e. { s e. ( F " r ) | A. t e. ( F " r ) -. t R s } )
21 6 ffnd 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> F Fn U_ x e. A B )
22 breq1 
 |-  ( t = ( F ` w ) -> ( t R s <-> ( F ` w ) R s ) )
23 22 notbid 
 |-  ( t = ( F ` w ) -> ( -. t R s <-> -. ( F ` w ) R s ) )
24 23 ralima 
 |-  ( ( F Fn U_ x e. A B /\ r C_ U_ x e. A B ) -> ( A. t e. ( F " r ) -. t R s <-> A. w e. r -. ( F ` w ) R s ) )
25 24 rabbidv 
 |-  ( ( F Fn U_ x e. A B /\ r C_ U_ x e. A B ) -> { s e. ( F " r ) | A. t e. ( F " r ) -. t R s } = { s e. ( F " r ) | A. w e. r -. ( F ` w ) R s } )
26 21 8 25 syl2anc 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> { s e. ( F " r ) | A. t e. ( F " r ) -. t R s } = { s e. ( F " r ) | A. w e. r -. ( F ` w ) R s } )
27 20 26 eleqtrd 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> C e. { s e. ( F " r ) | A. w e. r -. ( F ` w ) R s } )
28 nfriota1 
 |-  F/_ s ( iota_ s e. ( F " r ) A. t e. ( F " r ) -. t R s )
29 2 28 nfcxfr 
 |-  F/_ s C
30 nfcv 
 |-  F/_ s ( F " r )
31 nfcv 
 |-  F/_ s r
32 nfcv 
 |-  F/_ s ( F ` w )
33 nfcv 
 |-  F/_ s R
34 32 33 29 nfbr 
 |-  F/ s ( F ` w ) R C
35 34 nfn 
 |-  F/ s -. ( F ` w ) R C
36 31 35 nfralw 
 |-  F/ s A. w e. r -. ( F ` w ) R C
37 breq2 
 |-  ( s = C -> ( ( F ` w ) R s <-> ( F ` w ) R C ) )
38 37 notbid 
 |-  ( s = C -> ( -. ( F ` w ) R s <-> -. ( F ` w ) R C ) )
39 38 ralbidv 
 |-  ( s = C -> ( A. w e. r -. ( F ` w ) R s <-> A. w e. r -. ( F ` w ) R C ) )
40 29 30 36 39 elrabf 
 |-  ( C e. { s e. ( F " r ) | A. w e. r -. ( F ` w ) R s } <-> ( C e. ( F " r ) /\ A. w e. r -. ( F ` w ) R C ) )
41 27 40 sylib 
 |-  ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\ r =/= (/) ) ) -> ( C e. ( F " r ) /\ A. w e. r -. ( F ` w ) R C ) )