Theorem pwfseqlem2 9481

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

Hypotheses

Ref	Expression
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

Ref	Expression
pwfseqlem2	|- ( ( Y e. Fin /\ R e. V ) -> ( Y F R ) = ( H ` ( card ` Y ) ) )

Distinct variable groups:   n, r, w, x, z   D, n, z   w, G   w, K   H, r, x, z   ph, n, r, x, z   ps, n, z   A, n, r, x, z   V, r, x

Allowed substitution hints:   ph( w)   ps( x, w, r)   A( w)   D( x, w, r)   R( x, z, w, n, r)   F( x, z, w, n, r)   G( x, z, n, r)   H( w, n)   K( x, z, n, r)   V( z, w, n)   X( x, z, w, n, r)   Y( x, z, w, n, r)

Proof of Theorem pwfseqlem2

Dummy variables a s are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 6657	. . 3 |- ( a = Y -> ( a F s ) = ( Y F s ) )
2		fveq2 6191	. . . 4 |- ( a = Y -> ( card ` a ) = ( card ` Y ) )
3	2	fveq2d 6195	. . 3 |- ( a = Y -> ( H ` ( card ` a ) ) = ( H ` ( card ` Y ) ) )
4	1, 3	eqeq12d 2637	. 2 |- ( a = Y -> ( ( a F s ) = ( H ` ( card ` a ) ) <-> ( Y F s ) = ( H ` ( card ` Y ) ) ) )
5		oveq2 6658	. . 3 |- ( s = R -> ( Y F s ) = ( Y F R ) )
6	5	eqeq1d 2624	. 2 |- ( s = R -> ( ( Y F s ) = ( H ` ( card ` Y ) ) <-> ( Y F R ) = ( H ` ( card ` Y ) ) ) )
7		nfcv 2764	. . 3 |- F/_ x a
8		nfcv 2764	. . 3 |- F/_ r a
9		nfcv 2764	. . 3 |- F/_ r s
10		pwfseqlem4.f	. . . . . 6 |- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) )
11		nfmpt21 6722	. . . . . 6 |- F/_ x ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) )
12	10, 11	nfcxfr 2762	. . . . 5 |- F/_ x F
13		nfcv 2764	. . . . 5 |- F/_ x r
14	7, 12, 13	nfov 6676	. . . 4 |- F/_ x ( a F r )
15	14	nfeq1 2778	. . 3 |- F/ x ( a F r ) = ( H ` ( card ` a ) )
16		nfmpt22 6723	. . . . . 6 |- F/_ r ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) )
17	10, 16	nfcxfr 2762	. . . . 5 |- F/_ r F
18	8, 17, 9	nfov 6676	. . . 4 |- F/_ r ( a F s )
19	18	nfeq1 2778	. . 3 |- F/ r ( a F s ) = ( H ` ( card ` a ) )
20		oveq1 6657	. . . 4 |- ( x = a -> ( x F r ) = ( a F r ) )
21		fveq2 6191	. . . . 5 |- ( x = a -> ( card ` x ) = ( card ` a ) )
22	21	fveq2d 6195	. . . 4 |- ( x = a -> ( H ` ( card ` x ) ) = ( H ` ( card ` a ) ) )
23	20, 22	eqeq12d 2637	. . 3 |- ( x = a -> ( ( x F r ) = ( H ` ( card ` x ) ) <-> ( a F r ) = ( H ` ( card ` a ) ) ) )
24		oveq2 6658	. . . 4 |- ( r = s -> ( a F r ) = ( a F s ) )
25	24	eqeq1d 2624	. . 3 |- ( r = s -> ( ( a F r ) = ( H ` ( card ` a ) ) <-> ( a F s ) = ( H ` ( card ` a ) ) ) )
26		vex 3203	. . . . . 6 |- x e. _V
27		vex 3203	. . . . . 6 |- r e. _V
28		fvex 6201	. . . . . . 7 |- ( H ` ( card ` x ) ) e. _V
29		fvex 6201	. . . . . . 7 |- ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) e. _V
30	28, 29	ifex 4156	. . . . . 6 |- if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) e. _V
31	10	ovmpt4g 6783	. . . . . 6 |- ( ( 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 } ) ) )
32	26, 27, 30, 31	mp3an 1424	. . . . 5 |- ( x F r ) = if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) )
33		iftrue 4092	. . . . 5 |- ( x e. Fin -> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. om | -. ( D ` z ) e. x } ) ) = ( H ` ( card ` x ) ) )
34	32, 33	syl5eq 2668	. . . 4 |- ( x e. Fin -> ( x F r ) = ( H ` ( card ` x ) ) )
35	34	adantr 481	. . 3 |- ( ( x e. Fin /\ r e. V ) -> ( x F r ) = ( H ` ( card ` x ) ) )
36	7, 8, 9, 15, 19, 23, 25, 35	vtocl2gaf 3273	. 2 |- ( ( a e. Fin /\ s e. V ) -> ( a F s ) = ( H ` ( card ` a ) ) )
37	4, 6, 36	vtocl2ga 3274	1 |- ( ( Y e. Fin /\ R e. V ) -> ( Y F R ) = ( H ` ( card ` Y ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {crab 2916   _Vcvv 3200   C_ wss 3574   ifcif 4086   ~Pcpw 4158   |^|cint 4475   U_ciun 4520   class class class wbr 4653   We wwe 5072   X. cxp 5112   `'ccnv 5113   ran crn 5115   -1-1->wf1 5885   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   omcom 7065   ^m cmap 7857   ~<_ cdom 7953   Fincfn 7955   cardccrd 8761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  pwfseqlem4a  9483  pwfseqlem4  9484