Metamath Proof Explorer

Theorem tfrlem1

Description: A technical lemma for transfinite recursion. Compare Lemma 1 of TakeutiZaring p. 47. (Contributed by NM, 23-Mar-1995) (Revised by Mario Carneiro, 24-May-2019)

Ref Expression
Hypotheses tfrlem1.1 
|- ( ph -> A e. On )
tfrlem1.2 
|- ( ph -> ( Fun F /\ A C_ dom F ) )
tfrlem1.3 
|- ( ph -> ( Fun G /\ A C_ dom G ) )
tfrlem1.4 
|- ( ph -> A. x e. A ( F ` x ) = ( B ` ( F |` x ) ) )
tfrlem1.5 
|- ( ph -> A. x e. A ( G ` x ) = ( B ` ( G |` x ) ) )
Assertion tfrlem1 
|- ( ph -> A. x e. A ( F ` x ) = ( G ` x ) )

Proof

Step Hyp Ref Expression
1 tfrlem1.1 
 |-  ( ph -> A e. On )
2 tfrlem1.2 
 |-  ( ph -> ( Fun F /\ A C_ dom F ) )
3 tfrlem1.3 
 |-  ( ph -> ( Fun G /\ A C_ dom G ) )
4 tfrlem1.4 
 |-  ( ph -> A. x e. A ( F ` x ) = ( B ` ( F |` x ) ) )
5 tfrlem1.5 
 |-  ( ph -> A. x e. A ( G ` x ) = ( B ` ( G |` x ) ) )
6 ssid 
 |-  A C_ A
7 sseq1 
 |-  ( y = z -> ( y C_ A <-> z C_ A ) )
8 raleq 
 |-  ( y = z -> ( A. x e. y ( F ` x ) = ( G ` x ) <-> A. x e. z ( F ` x ) = ( G ` x ) ) )
9 7 8 imbi12d 
 |-  ( y = z -> ( ( y C_ A -> A. x e. y ( F ` x ) = ( G ` x ) ) <-> ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) )
10 9 imbi2d 
 |-  ( y = z -> ( ( ph -> ( y C_ A -> A. x e. y ( F ` x ) = ( G ` x ) ) ) <-> ( ph -> ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) ) )
11 sseq1 
 |-  ( y = A -> ( y C_ A <-> A C_ A ) )
12 raleq 
 |-  ( y = A -> ( A. x e. y ( F ` x ) = ( G ` x ) <-> A. x e. A ( F ` x ) = ( G ` x ) ) )
13 11 12 imbi12d 
 |-  ( y = A -> ( ( y C_ A -> A. x e. y ( F ` x ) = ( G ` x ) ) <-> ( A C_ A -> A. x e. A ( F ` x ) = ( G ` x ) ) ) )
14 13 imbi2d 
 |-  ( y = A -> ( ( ph -> ( y C_ A -> A. x e. y ( F ` x ) = ( G ` x ) ) ) <-> ( ph -> ( A C_ A -> A. x e. A ( F ` x ) = ( G ` x ) ) ) ) )
15 r19.21v 
 |-  ( A. z e. y ( ph -> ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) <-> ( ph -> A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) )
16 2 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( Fun F /\ A C_ dom F ) )
17 16 simpld 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> Fun F )
18 17 funfnd 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> F Fn dom F )
19 eloni 
 |-  ( y e. On -> Ord y )
20 19 ad3antlr 
 |-  ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) -> Ord y )
21 ordelss 
 |-  ( ( Ord y /\ w e. y ) -> w C_ y )
22 20 21 sylan 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> w C_ y )
23 simplr 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> y C_ A )
24 22 23 sstrd 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> w C_ A )
25 16 simprd 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> A C_ dom F )
26 24 25 sstrd 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> w C_ dom F )
27 fnssres 
 |-  ( ( F Fn dom F /\ w C_ dom F ) -> ( F |` w ) Fn w )
28 18 26 27 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( F |` w ) Fn w )
29 3 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( Fun G /\ A C_ dom G ) )
30 29 simpld 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> Fun G )
31 30 funfnd 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> G Fn dom G )
32 29 simprd 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> A C_ dom G )
33 24 32 sstrd 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> w C_ dom G )
34 fnssres 
 |-  ( ( G Fn dom G /\ w C_ dom G ) -> ( G |` w ) Fn w )
35 31 33 34 syl2anc 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( G |` w ) Fn w )
36 fveq2 
 |-  ( x = u -> ( F ` x ) = ( F ` u ) )
37 fveq2 
 |-  ( x = u -> ( G ` x ) = ( G ` u ) )
38 36 37 eqeq12d 
 |-  ( x = u -> ( ( F ` x ) = ( G ` x ) <-> ( F ` u ) = ( G ` u ) ) )
39 24 adantr 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> w C_ A )
40 sseq1 
 |-  ( z = w -> ( z C_ A <-> w C_ A ) )
41 raleq 
 |-  ( z = w -> ( A. x e. z ( F ` x ) = ( G ` x ) <-> A. x e. w ( F ` x ) = ( G ` x ) ) )
42 40 41 imbi12d 
 |-  ( z = w -> ( ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) <-> ( w C_ A -> A. x e. w ( F ` x ) = ( G ` x ) ) ) )
43 simp-4r 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) )
44 simplr 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> w e. y )
45 42 43 44 rspcdva 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> ( w C_ A -> A. x e. w ( F ` x ) = ( G ` x ) ) )
46 39 45 mpd 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> A. x e. w ( F ` x ) = ( G ` x ) )
47 simpr 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> u e. w )
48 38 46 47 rspcdva 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> ( F ` u ) = ( G ` u ) )
49 fvres 
 |-  ( u e. w -> ( ( F |` w ) ` u ) = ( F ` u ) )
50 49 adantl 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> ( ( F |` w ) ` u ) = ( F ` u ) )
51 fvres 
 |-  ( u e. w -> ( ( G |` w ) ` u ) = ( G ` u ) )
52 51 adantl 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> ( ( G |` w ) ` u ) = ( G ` u ) )
53 48 50 52 3eqtr4d 
 |-  ( ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) /\ u e. w ) -> ( ( F |` w ) ` u ) = ( ( G |` w ) ` u ) )
54 28 35 53 eqfnfvd 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( F |` w ) = ( G |` w ) )
55 54 fveq2d 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( B ` ( F |` w ) ) = ( B ` ( G |` w ) ) )
56 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
57 reseq2 
 |-  ( x = w -> ( F |` x ) = ( F |` w ) )
58 57 fveq2d 
 |-  ( x = w -> ( B ` ( F |` x ) ) = ( B ` ( F |` w ) ) )
59 56 58 eqeq12d 
 |-  ( x = w -> ( ( F ` x ) = ( B ` ( F |` x ) ) <-> ( F ` w ) = ( B ` ( F |` w ) ) ) )
60 4 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> A. x e. A ( F ` x ) = ( B ` ( F |` x ) ) )
61 simpr 
 |-  ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) -> y C_ A )
62 61 sselda 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> w e. A )
63 59 60 62 rspcdva 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( F ` w ) = ( B ` ( F |` w ) ) )
64 fveq2 
 |-  ( x = w -> ( G ` x ) = ( G ` w ) )
65 reseq2 
 |-  ( x = w -> ( G |` x ) = ( G |` w ) )
66 65 fveq2d 
 |-  ( x = w -> ( B ` ( G |` x ) ) = ( B ` ( G |` w ) ) )
67 64 66 eqeq12d 
 |-  ( x = w -> ( ( G ` x ) = ( B ` ( G |` x ) ) <-> ( G ` w ) = ( B ` ( G |` w ) ) ) )
68 5 ad4antr 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> A. x e. A ( G ` x ) = ( B ` ( G |` x ) ) )
69 67 68 62 rspcdva 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( G ` w ) = ( B ` ( G |` w ) ) )
70 55 63 69 3eqtr4d 
 |-  ( ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) /\ w e. y ) -> ( F ` w ) = ( G ` w ) )
71 70 ralrimiva 
 |-  ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) -> A. w e. y ( F ` w ) = ( G ` w ) )
72 56 64 eqeq12d 
 |-  ( x = w -> ( ( F ` x ) = ( G ` x ) <-> ( F ` w ) = ( G ` w ) ) )
73 72 cbvralvw 
 |-  ( A. x e. y ( F ` x ) = ( G ` x ) <-> A. w e. y ( F ` w ) = ( G ` w ) )
74 71 73 sylibr 
 |-  ( ( ( ( ph /\ y e. On ) /\ A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) /\ y C_ A ) -> A. x e. y ( F ` x ) = ( G ` x ) )
75 74 exp31 
 |-  ( ( ph /\ y e. On ) -> ( A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) -> ( y C_ A -> A. x e. y ( F ` x ) = ( G ` x ) ) ) )
76 75 expcom 
 |-  ( y e. On -> ( ph -> ( A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) -> ( y C_ A -> A. x e. y ( F ` x ) = ( G ` x ) ) ) ) )
77 76 a2d 
 |-  ( y e. On -> ( ( ph -> A. z e. y ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) -> ( ph -> ( y C_ A -> A. x e. y ( F ` x ) = ( G ` x ) ) ) ) )
78 15 77 syl5bi 
 |-  ( y e. On -> ( A. z e. y ( ph -> ( z C_ A -> A. x e. z ( F ` x ) = ( G ` x ) ) ) -> ( ph -> ( y C_ A -> A. x e. y ( F ` x ) = ( G ` x ) ) ) ) )
79 10 14 78 tfis3 
 |-  ( A e. On -> ( ph -> ( A C_ A -> A. x e. A ( F ` x ) = ( G ` x ) ) ) )
80 1 79 mpcom 
 |-  ( ph -> ( A C_ A -> A. x e. A ( F ` x ) = ( G ` x ) ) )
81 6 80 mpi 
 |-  ( ph -> A. x e. A ( F ` x ) = ( G ` x ) )