Metamath Proof Explorer

Theorem pwfseqlem2

Description: Lemma for pwfseq . (Contributed by Mario Carneiro, 18-Nov-2014) (Revised by AV, 18-Sep-2021)

Ref Expression
Hypotheses pwfseqlem4.g 
|- ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
pwfseqlem4.x 
|- ( ph -> X C_ A )
pwfseqlem4.h 
|- ( ph -> H : _om -1-1-onto-> X )
pwfseqlem4.ps 
|- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) )
pwfseqlem4.k 
|- ( ( ph /\ ps ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x )
pwfseqlem4.d 
|- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
pwfseqlem4.f 
|- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
Assertion pwfseqlem2 
|- ( ( Y e. Fin /\ R e. V ) -> ( Y F R ) = ( H ` ( card ` Y ) ) )

Proof

Step Hyp Ref Expression
1 pwfseqlem4.g 
 |-  ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
2 pwfseqlem4.x 
 |-  ( ph -> X C_ A )
3 pwfseqlem4.h 
 |-  ( ph -> H : _om -1-1-onto-> X )
4 pwfseqlem4.ps 
 |-  ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) )
5 pwfseqlem4.k 
 |-  ( ( ph /\ ps ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x )
6 pwfseqlem4.d 
 |-  D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
7 pwfseqlem4.f 
 |-  F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
8 oveq1 
 |-  ( a = Y -> ( a F s ) = ( Y F s ) )
9 2fveq3 
 |-  ( a = Y -> ( H ` ( card ` a ) ) = ( H ` ( card ` Y ) ) )
10 8 9 eqeq12d 
 |-  ( a = Y -> ( ( a F s ) = ( H ` ( card ` a ) ) <-> ( Y F s ) = ( H ` ( card ` Y ) ) ) )
11 oveq2 
 |-  ( s = R -> ( Y F s ) = ( Y F R ) )
12 11 eqeq1d 
 |-  ( s = R -> ( ( Y F s ) = ( H ` ( card ` Y ) ) <-> ( Y F R ) = ( H ` ( card ` Y ) ) ) )
13 nfcv 
 |-  F/_ x a
14 nfcv 
 |-  F/_ r a
15 nfcv 
 |-  F/_ r s
16 nfmpo1 
 |-  F/_ x ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
17 7 16 nfcxfr 
 |-  F/_ x F
18 nfcv 
 |-  F/_ x r
19 13 17 18 nfov 
 |-  F/_ x ( a F r )
20 19 nfeq1 
 |-  F/ x ( a F r ) = ( H ` ( card ` a ) )
21 nfmpo2 
 |-  F/_ r ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
22 7 21 nfcxfr 
 |-  F/_ r F
23 14 22 15 nfov 
 |-  F/_ r ( a F s )
24 23 nfeq1 
 |-  F/ r ( a F s ) = ( H ` ( card ` a ) )
25 oveq1 
 |-  ( x = a -> ( x F r ) = ( a F r ) )
26 2fveq3 
 |-  ( x = a -> ( H ` ( card ` x ) ) = ( H ` ( card ` a ) ) )
27 25 26 eqeq12d 
 |-  ( x = a -> ( ( x F r ) = ( H ` ( card ` x ) ) <-> ( a F r ) = ( H ` ( card ` a ) ) ) )
28 oveq2 
 |-  ( r = s -> ( a F r ) = ( a F s ) )
29 28 eqeq1d 
 |-  ( r = s -> ( ( a F r ) = ( H ` ( card ` a ) ) <-> ( a F s ) = ( H ` ( card ` a ) ) ) )
30 vex 
 |-  x e. _V
31 vex 
 |-  r e. _V
32 fvex 
 |-  ( H ` ( card ` x ) ) e. _V
33 fvex 
 |-  ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) e. _V
34 32 33 ifex 
 |-  if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) e. _V
35 7 ovmpt4g 
 |-  ( ( x e. _V /\ r e. _V /\ if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) e. _V ) -> ( x F r ) = if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
36 30 31 34 35 mp3an 
 |-  ( x F r ) = if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) )
37 iftrue 
 |-  ( x e. Fin -> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) = ( H ` ( card ` x ) ) )
38 36 37 syl5eq 
 |-  ( x e. Fin -> ( x F r ) = ( H ` ( card ` x ) ) )
39 38 adantr 
 |-  ( ( x e. Fin /\ r e. V ) -> ( x F r ) = ( H ` ( card ` x ) ) )
40 13 14 15 20 24 27 29 39 vtocl2gaf 
 |-  ( ( a e. Fin /\ s e. V ) -> ( a F s ) = ( H ` ( card ` a ) ) )
41 10 12 40 vtocl2ga 
 |-  ( ( Y e. Fin /\ R e. V ) -> ( Y F R ) = ( H ` ( card ` Y ) ) )