Metamath Proof Explorer

Theorem exrecfnlem

Description: Lemma for exrecfn . (Contributed by ML, 30-Mar-2022)

Ref Expression
Hypothesis exrecfnlem.1 
|- F = ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) )
Assertion exrecfnlem 
|- ( ( A e. V /\ A. y B e. W ) -> E. x ( A C_ x /\ A. y e. x B e. x ) )

Proof

Step Hyp Ref Expression
1 exrecfnlem.1 
 |-  F = ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) )
2 rdg0g 
 |-  ( A e. V -> ( rec ( F , A ) ` (/) ) = A )
3 peano1 
 |-  (/) e. _om
4 omelon 
 |-  _om e. On
5 limom 
 |-  Lim _om
6 rdglimss 
 |-  ( ( ( _om e. On /\ Lim _om ) /\ (/) e. _om ) -> ( rec ( F , A ) ` (/) ) C_ ( rec ( F , A ) ` _om ) )
7 4 5 6 mpanl12 
 |-  ( (/) e. _om -> ( rec ( F , A ) ` (/) ) C_ ( rec ( F , A ) ` _om ) )
8 3 7 ax-mp 
 |-  ( rec ( F , A ) ` (/) ) C_ ( rec ( F , A ) ` _om )
9 2 8 eqsstrrdi 
 |-  ( A e. V -> A C_ ( rec ( F , A ) ` _om ) )
10 rdglim2a 
 |-  ( ( _om e. On /\ Lim _om ) -> ( rec ( F , A ) ` _om ) = U_ u e. _om ( rec ( F , A ) ` u ) )
11 4 5 10 mp2an 
 |-  ( rec ( F , A ) ` _om ) = U_ u e. _om ( rec ( F , A ) ` u )
12 11 eleq2i 
 |-  ( y e. ( rec ( F , A ) ` _om ) <-> y e. U_ u e. _om ( rec ( F , A ) ` u ) )
13 eliun 
 |-  ( y e. U_ u e. _om ( rec ( F , A ) ` u ) <-> E. u e. _om y e. ( rec ( F , A ) ` u ) )
14 12 13 bitri 
 |-  ( y e. ( rec ( F , A ) ` _om ) <-> E. u e. _om y e. ( rec ( F , A ) ` u ) )
15 peano2 
 |-  ( u e. _om -> suc u e. _om )
16 nnon 
 |-  ( u e. _om -> u e. On )
17 eqid 
 |-  ( y e. ( rec ( F , A ) ` u ) |-> B ) = ( y e. ( rec ( F , A ) ` u ) |-> B )
18 17 elrnmpt1 
 |-  ( ( y e. ( rec ( F , A ) ` u ) /\ B e. W ) -> B e. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) )
19 elun2 
 |-  ( B e. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) -> B e. ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) ) )
20 18 19 syl 
 |-  ( ( y e. ( rec ( F , A ) ` u ) /\ B e. W ) -> B e. ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) ) )
21 fvex 
 |-  ( rec ( F , A ) ` u ) e. _V
22 nfcv 
 |-  F/_ y _V
23 nfcv 
 |-  F/_ y z
24 nfmpt1 
 |-  F/_ y ( y e. z |-> B )
25 24 nfrn 
 |-  F/_ y ran ( y e. z |-> B )
26 23 25 nfun 
 |-  F/_ y ( z u. ran ( y e. z |-> B ) )
27 22 26 nfmpt 
 |-  F/_ y ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) )
28 1 27 nfcxfr 
 |-  F/_ y F
29 nfcv 
 |-  F/_ y A
30 28 29 nfrdg 
 |-  F/_ y rec ( F , A )
31 nfcv 
 |-  F/_ y u
32 30 31 nffv 
 |-  F/_ y ( rec ( F , A ) ` u )
33 32 mptexgf 
 |-  ( ( rec ( F , A ) ` u ) e. _V -> ( y e. ( rec ( F , A ) ` u ) |-> B ) e. _V )
34 21 33 ax-mp 
 |-  ( y e. ( rec ( F , A ) ` u ) |-> B ) e. _V
35 34 rnex 
 |-  ran ( y e. ( rec ( F , A ) ` u ) |-> B ) e. _V
36 21 35 unex 
 |-  ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) ) e. _V
37 nfcv 
 |-  F/_ z A
38 nfcv 
 |-  F/_ z u
39 nfmpt1 
 |-  F/_ z ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) )
40 1 39 nfcxfr 
 |-  F/_ z F
41 40 37 nfrdg 
 |-  F/_ z rec ( F , A )
42 41 38 nffv 
 |-  F/_ z ( rec ( F , A ) ` u )
43 nfcv 
 |-  F/_ z B
44 42 43 nfmpt 
 |-  F/_ z ( y e. ( rec ( F , A ) ` u ) |-> B )
45 44 nfrn 
 |-  F/_ z ran ( y e. ( rec ( F , A ) ` u ) |-> B )
46 42 45 nfun 
 |-  F/_ z ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) )
47 rdgeq1 
 |-  ( F = ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) ) -> rec ( F , A ) = rec ( ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) ) , A ) )
48 1 47 ax-mp 
 |-  rec ( F , A ) = rec ( ( z e. _V |-> ( z u. ran ( y e. z |-> B ) ) ) , A )
49 id 
 |-  ( z = ( rec ( F , A ) ` u ) -> z = ( rec ( F , A ) ` u ) )
50 32 nfeq2 
 |-  F/ y z = ( rec ( F , A ) ` u )
51 eqidd 
 |-  ( z = ( rec ( F , A ) ` u ) -> B = B )
52 50 49 51 mpteq12df 
 |-  ( z = ( rec ( F , A ) ` u ) -> ( y e. z |-> B ) = ( y e. ( rec ( F , A ) ` u ) |-> B ) )
53 52 rneqd 
 |-  ( z = ( rec ( F , A ) ` u ) -> ran ( y e. z |-> B ) = ran ( y e. ( rec ( F , A ) ` u ) |-> B ) )
54 49 53 uneq12d 
 |-  ( z = ( rec ( F , A ) ` u ) -> ( z u. ran ( y e. z |-> B ) ) = ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) ) )
55 37 38 46 48 54 rdgsucmptf 
 |-  ( ( u e. On /\ ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) ) e. _V ) -> ( rec ( F , A ) ` suc u ) = ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) ) )
56 36 55 mpan2 
 |-  ( u e. On -> ( rec ( F , A ) ` suc u ) = ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) ) )
57 56 eleq2d 
 |-  ( u e. On -> ( B e. ( rec ( F , A ) ` suc u ) <-> B e. ( ( rec ( F , A ) ` u ) u. ran ( y e. ( rec ( F , A ) ` u ) |-> B ) ) ) )
58 20 57 syl5ibr 
 |-  ( u e. On -> ( ( y e. ( rec ( F , A ) ` u ) /\ B e. W ) -> B e. ( rec ( F , A ) ` suc u ) ) )
59 16 58 syl 
 |-  ( u e. _om -> ( ( y e. ( rec ( F , A ) ` u ) /\ B e. W ) -> B e. ( rec ( F , A ) ` suc u ) ) )
60 rdgellim 
 |-  ( ( ( _om e. On /\ Lim _om ) /\ suc u e. _om ) -> ( B e. ( rec ( F , A ) ` suc u ) -> B e. ( rec ( F , A ) ` _om ) ) )
61 4 5 60 mpanl12 
 |-  ( suc u e. _om -> ( B e. ( rec ( F , A ) ` suc u ) -> B e. ( rec ( F , A ) ` _om ) ) )
62 15 59 61 sylsyld 
 |-  ( u e. _om -> ( ( y e. ( rec ( F , A ) ` u ) /\ B e. W ) -> B e. ( rec ( F , A ) ` _om ) ) )
63 62 expd 
 |-  ( u e. _om -> ( y e. ( rec ( F , A ) ` u ) -> ( B e. W -> B e. ( rec ( F , A ) ` _om ) ) ) )
64 63 com3r 
 |-  ( B e. W -> ( u e. _om -> ( y e. ( rec ( F , A ) ` u ) -> B e. ( rec ( F , A ) ` _om ) ) ) )
65 64 rexlimdv 
 |-  ( B e. W -> ( E. u e. _om y e. ( rec ( F , A ) ` u ) -> B e. ( rec ( F , A ) ` _om ) ) )
66 14 65 syl5bi 
 |-  ( B e. W -> ( y e. ( rec ( F , A ) ` _om ) -> B e. ( rec ( F , A ) ` _om ) ) )
67 66 alimi 
 |-  ( A. y B e. W -> A. y ( y e. ( rec ( F , A ) ` _om ) -> B e. ( rec ( F , A ) ` _om ) ) )
68 df-ral 
 |-  ( A. y e. ( rec ( F , A ) ` _om ) B e. ( rec ( F , A ) ` _om ) <-> A. y ( y e. ( rec ( F , A ) ` _om ) -> B e. ( rec ( F , A ) ` _om ) ) )
69 67 68 sylibr 
 |-  ( A. y B e. W -> A. y e. ( rec ( F , A ) ` _om ) B e. ( rec ( F , A ) ` _om ) )
70 fvex 
 |-  ( rec ( F , A ) ` _om ) e. _V
71 sseq2 
 |-  ( x = ( rec ( F , A ) ` _om ) -> ( A C_ x <-> A C_ ( rec ( F , A ) ` _om ) ) )
72 nfcv 
 |-  F/_ y _om
73 30 72 nffv 
 |-  F/_ y ( rec ( F , A ) ` _om )
74 73 nfeq2 
 |-  F/ y x = ( rec ( F , A ) ` _om )
75 eleq2 
 |-  ( x = ( rec ( F , A ) ` _om ) -> ( y e. x <-> y e. ( rec ( F , A ) ` _om ) ) )
76 eleq2 
 |-  ( x = ( rec ( F , A ) ` _om ) -> ( B e. x <-> B e. ( rec ( F , A ) ` _om ) ) )
77 75 76 imbi12d 
 |-  ( x = ( rec ( F , A ) ` _om ) -> ( ( y e. x -> B e. x ) <-> ( y e. ( rec ( F , A ) ` _om ) -> B e. ( rec ( F , A ) ` _om ) ) ) )
78 74 77 albid 
 |-  ( x = ( rec ( F , A ) ` _om ) -> ( A. y ( y e. x -> B e. x ) <-> A. y ( y e. ( rec ( F , A ) ` _om ) -> B e. ( rec ( F , A ) ` _om ) ) ) )
79 df-ral 
 |-  ( A. y e. x B e. x <-> A. y ( y e. x -> B e. x ) )
80 78 79 68 3bitr4g 
 |-  ( x = ( rec ( F , A ) ` _om ) -> ( A. y e. x B e. x <-> A. y e. ( rec ( F , A ) ` _om ) B e. ( rec ( F , A ) ` _om ) ) )
81 71 80 anbi12d 
 |-  ( x = ( rec ( F , A ) ` _om ) -> ( ( A C_ x /\ A. y e. x B e. x ) <-> ( A C_ ( rec ( F , A ) ` _om ) /\ A. y e. ( rec ( F , A ) ` _om ) B e. ( rec ( F , A ) ` _om ) ) ) )
82 70 81 spcev 
 |-  ( ( A C_ ( rec ( F , A ) ` _om ) /\ A. y e. ( rec ( F , A ) ` _om ) B e. ( rec ( F , A ) ` _om ) ) -> E. x ( A C_ x /\ A. y e. x B e. x ) )
83 9 69 82 syl2an 
 |-  ( ( A e. V /\ A. y B e. W ) -> E. x ( A C_ x /\ A. y e. x B e. x ) )