Metamath Proof Explorer

Theorem weiunlem2

Description: Lemma for weiunpo , weiunso , and weiunse . (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Hypothesis weiunlem2.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 ) )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 weiunlem2.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 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 ) ) ) )
3 biid 
 |-  ( F : U_ x e. A B --> A <-> F : U_ x e. A B --> A )
4 nfv 
 |-  F/ t w e. [_ ( F ` w ) / x ]_ B
5 nfmpt1 
 |-  F/_ w ( 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 ) )
6 1 5 nfcxfr 
 |-  F/_ w F
7 nfcv 
 |-  F/_ w t
8 6 7 nffv 
 |-  F/_ w ( F ` t )
9 nfcv 
 |-  F/_ w B
10 8 9 nfcsbw 
 |-  F/_ w [_ ( F ` t ) / x ]_ B
11 10 nfcri 
 |-  F/ w t e. [_ ( F ` t ) / x ]_ B
12 id 
 |-  ( w = t -> w = t )
13 fveq2 
 |-  ( w = t -> ( F ` w ) = ( F ` t ) )
14 13 csbeq1d 
 |-  ( w = t -> [_ ( F ` w ) / x ]_ B = [_ ( F ` t ) / x ]_ B )
15 12 14 eleq12d 
 |-  ( w = t -> ( w e. [_ ( F ` w ) / x ]_ B <-> t e. [_ ( F ` t ) / x ]_ B ) )
16 4 11 15 cbvralw 
 |-  ( A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B <-> A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B )
17 nfv 
 |-  F/ t A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) )
18 nfcv 
 |-  F/_ w A
19 nfv 
 |-  F/ w t e. [_ s / x ]_ B
20 nfcv 
 |-  F/_ w s
21 nfcv 
 |-  F/_ w R
22 20 21 8 nfbr 
 |-  F/ w s R ( F ` t )
23 22 nfn 
 |-  F/ w -. s R ( F ` t )
24 19 23 nfim 
 |-  F/ w ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) )
25 18 24 nfralw 
 |-  F/ w A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) )
26 nfv 
 |-  F/ s ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) )
27 nfv 
 |-  F/ v w e. [_ s / x ]_ B
28 nfcv 
 |-  F/_ v s
29 nfcv 
 |-  F/_ v R
30 nfcv 
 |-  F/_ v U_ x e. A B
31 nfra1 
 |-  F/ v A. v e. { x e. A | w e. B } -. v R u
32 nfcv 
 |-  F/_ v { x e. A | w e. B }
33 31 32 nfriota 
 |-  F/_ v ( iota_ u e. { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u )
34 30 33 nfmpt 
 |-  F/_ v ( 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 ) )
35 1 34 nfcxfr 
 |-  F/_ v F
36 nfcv 
 |-  F/_ v w
37 35 36 nffv 
 |-  F/_ v ( F ` w )
38 28 29 37 nfbr 
 |-  F/ v s R ( F ` w )
39 38 nfn 
 |-  F/ v -. s R ( F ` w )
40 27 39 nfim 
 |-  F/ v ( w e. [_ s / x ]_ B -> -. s R ( F ` w ) )
41 csbeq1 
 |-  ( v = s -> [_ v / x ]_ B = [_ s / x ]_ B )
42 41 eleq2d 
 |-  ( v = s -> ( w e. [_ v / x ]_ B <-> w e. [_ s / x ]_ B ) )
43 breq1 
 |-  ( v = s -> ( v R ( F ` w ) <-> s R ( F ` w ) ) )
44 43 notbid 
 |-  ( v = s -> ( -. v R ( F ` w ) <-> -. s R ( F ` w ) ) )
45 42 44 imbi12d 
 |-  ( v = s -> ( ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) <-> ( w e. [_ s / x ]_ B -> -. s R ( F ` w ) ) ) )
46 26 40 45 cbvralw 
 |-  ( A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) <-> A. s e. A ( w e. [_ s / x ]_ B -> -. s R ( F ` w ) ) )
47 eleq1w 
 |-  ( w = t -> ( w e. [_ s / x ]_ B <-> t e. [_ s / x ]_ B ) )
48 13 breq2d 
 |-  ( w = t -> ( s R ( F ` w ) <-> s R ( F ` t ) ) )
49 48 notbid 
 |-  ( w = t -> ( -. s R ( F ` w ) <-> -. s R ( F ` t ) ) )
50 47 49 imbi12d 
 |-  ( w = t -> ( ( w e. [_ s / x ]_ B -> -. s R ( F ` w ) ) <-> ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) ) )
51 50 ralbidv 
 |-  ( w = t -> ( A. s e. A ( w e. [_ s / x ]_ B -> -. s R ( F ` w ) ) <-> A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) ) )
52 46 51 bitrid 
 |-  ( w = t -> ( A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) <-> A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) ) )
53 17 25 52 cbvralw 
 |-  ( A. w e. U_ x e. A B A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) <-> A. t e. U_ x e. A B A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) )
54 3 16 53 3anbi123i 
 |-  ( ( 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 ) ) ) <-> ( 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 ) ) ) )
55 2 54 sylib 
 |-  ( ( 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 ) ) ) )