Metamath Proof Explorer

Theorem fpwwe2lem7

Description: Lemma for fpwwe2 . Show by induction that the two isometries M and N agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe2.1 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
fpwwe2.2 
|- ( ph -> A e. V )
fpwwe2.3 
|- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
fpwwe2lem8.x 
|- ( ph -> X W R )
fpwwe2lem8.y 
|- ( ph -> Y W S )
fpwwe2lem8.m 
|- M = OrdIso ( R , X )
fpwwe2lem8.n 
|- N = OrdIso ( S , Y )
fpwwe2lem8.s 
|- ( ph -> dom M C_ dom N )
Assertion fpwwe2lem7 
|- ( ph -> M = ( N |` dom M ) )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 
 |-  W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
2 fpwwe2.2 
 |-  ( ph -> A e. V )
3 fpwwe2.3 
 |-  ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
4 fpwwe2lem8.x 
 |-  ( ph -> X W R )
5 fpwwe2lem8.y 
 |-  ( ph -> Y W S )
6 fpwwe2lem8.m 
 |-  M = OrdIso ( R , X )
7 fpwwe2lem8.n 
 |-  N = OrdIso ( S , Y )
8 fpwwe2lem8.s 
 |-  ( ph -> dom M C_ dom N )
9 6 oif 
 |-  M : dom M --> X
10 ffn 
 |-  ( M : dom M --> X -> M Fn dom M )
11 9 10 mp1i 
 |-  ( ph -> M Fn dom M )
12 7 oif 
 |-  N : dom N --> Y
13 ffn 
 |-  ( N : dom N --> Y -> N Fn dom N )
14 12 13 mp1i 
 |-  ( ph -> N Fn dom N )
15 14 8 fnssresd 
 |-  ( ph -> ( N |` dom M ) Fn dom M )
16 6 oicl 
 |-  Ord dom M
17 ordelon 
 |-  ( ( Ord dom M /\ w e. dom M ) -> w e. On )
18 16 17 mpan 
 |-  ( w e. dom M -> w e. On )
19 eleq1w 
 |-  ( w = y -> ( w e. dom M <-> y e. dom M ) )
20 fveq2 
 |-  ( w = y -> ( M ` w ) = ( M ` y ) )
21 fveq2 
 |-  ( w = y -> ( N ` w ) = ( N ` y ) )
22 20 21 eqeq12d 
 |-  ( w = y -> ( ( M ` w ) = ( N ` w ) <-> ( M ` y ) = ( N ` y ) ) )
23 19 22 imbi12d 
 |-  ( w = y -> ( ( w e. dom M -> ( M ` w ) = ( N ` w ) ) <-> ( y e. dom M -> ( M ` y ) = ( N ` y ) ) ) )
24 23 imbi2d 
 |-  ( w = y -> ( ( ph -> ( w e. dom M -> ( M ` w ) = ( N ` w ) ) ) <-> ( ph -> ( y e. dom M -> ( M ` y ) = ( N ` y ) ) ) ) )
25 r19.21v 
 |-  ( A. y e. w ( ph -> ( y e. dom M -> ( M ` y ) = ( N ` y ) ) ) <-> ( ph -> A. y e. w ( y e. dom M -> ( M ` y ) = ( N ` y ) ) ) )
26 16 a1i 
 |-  ( ph -> Ord dom M )
27 ordelss 
 |-  ( ( Ord dom M /\ w e. dom M ) -> w C_ dom M )
28 26 27 sylan 
 |-  ( ( ph /\ w e. dom M ) -> w C_ dom M )
29 28 sselda 
 |-  ( ( ( ph /\ w e. dom M ) /\ y e. w ) -> y e. dom M )
30 pm2.27 
 |-  ( y e. dom M -> ( ( y e. dom M -> ( M ` y ) = ( N ` y ) ) -> ( M ` y ) = ( N ` y ) ) )
31 29 30 syl 
 |-  ( ( ( ph /\ w e. dom M ) /\ y e. w ) -> ( ( y e. dom M -> ( M ` y ) = ( N ` y ) ) -> ( M ` y ) = ( N ` y ) ) )
32 31 ralimdva 
 |-  ( ( ph /\ w e. dom M ) -> ( A. y e. w ( y e. dom M -> ( M ` y ) = ( N ` y ) ) -> A. y e. w ( M ` y ) = ( N ` y ) ) )
33 fnssres 
 |-  ( ( M Fn dom M /\ w C_ dom M ) -> ( M |` w ) Fn w )
34 11 28 33 syl2an2r 
 |-  ( ( ph /\ w e. dom M ) -> ( M |` w ) Fn w )
35 8 adantr 
 |-  ( ( ph /\ w e. dom M ) -> dom M C_ dom N )
36 28 35 sstrd 
 |-  ( ( ph /\ w e. dom M ) -> w C_ dom N )
37 fnssres 
 |-  ( ( N Fn dom N /\ w C_ dom N ) -> ( N |` w ) Fn w )
38 14 36 37 syl2an2r 
 |-  ( ( ph /\ w e. dom M ) -> ( N |` w ) Fn w )
39 eqfnfv 
 |-  ( ( ( M |` w ) Fn w /\ ( N |` w ) Fn w ) -> ( ( M |` w ) = ( N |` w ) <-> A. y e. w ( ( M |` w ) ` y ) = ( ( N |` w ) ` y ) ) )
40 34 38 39 syl2anc 
 |-  ( ( ph /\ w e. dom M ) -> ( ( M |` w ) = ( N |` w ) <-> A. y e. w ( ( M |` w ) ` y ) = ( ( N |` w ) ` y ) ) )
41 fvres 
 |-  ( y e. w -> ( ( M |` w ) ` y ) = ( M ` y ) )
42 fvres 
 |-  ( y e. w -> ( ( N |` w ) ` y ) = ( N ` y ) )
43 41 42 eqeq12d 
 |-  ( y e. w -> ( ( ( M |` w ) ` y ) = ( ( N |` w ) ` y ) <-> ( M ` y ) = ( N ` y ) ) )
44 43 ralbiia 
 |-  ( A. y e. w ( ( M |` w ) ` y ) = ( ( N |` w ) ` y ) <-> A. y e. w ( M ` y ) = ( N ` y ) )
45 40 44 bitrdi 
 |-  ( ( ph /\ w e. dom M ) -> ( ( M |` w ) = ( N |` w ) <-> A. y e. w ( M ` y ) = ( N ` y ) ) )
46 2 ad2antrr 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> A e. V )
47 simpll 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ph )
48 47 3 sylan 
 |-  ( ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
49 4 ad2antrr 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> X W R )
50 5 ad2antrr 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> Y W S )
51 simplr 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> w e. dom M )
52 8 sselda 
 |-  ( ( ph /\ w e. dom M ) -> w e. dom N )
53 52 adantr 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> w e. dom N )
54 simpr 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( M |` w ) = ( N |` w ) )
55 1 46 48 49 50 6 7 51 53 54 fpwwe2lem6 
 |-  ( ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) /\ y R ( M ` w ) ) -> ( y S ( N ` w ) /\ ( z R ( M ` w ) -> ( y R z <-> y S z ) ) ) )
56 55 simpld 
 |-  ( ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) /\ y R ( M ` w ) ) -> y S ( N ` w ) )
57 54 eqcomd 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( N |` w ) = ( M |` w ) )
58 1 46 48 50 49 7 6 53 51 57 fpwwe2lem6 
 |-  ( ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) /\ y S ( N ` w ) ) -> ( y R ( M ` w ) /\ ( z S ( N ` w ) -> ( y S z <-> y R z ) ) ) )
59 58 simpld 
 |-  ( ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) /\ y S ( N ` w ) ) -> y R ( M ` w ) )
60 56 59 impbida 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( y R ( M ` w ) <-> y S ( N ` w ) ) )
61 fvex 
 |-  ( M ` w ) e. _V
62 vex 
 |-  y e. _V
63 62 eliniseg 
 |-  ( ( M ` w ) e. _V -> ( y e. ( `' R " { ( M ` w ) } ) <-> y R ( M ` w ) ) )
64 61 63 ax-mp 
 |-  ( y e. ( `' R " { ( M ` w ) } ) <-> y R ( M ` w ) )
65 fvex 
 |-  ( N ` w ) e. _V
66 62 eliniseg 
 |-  ( ( N ` w ) e. _V -> ( y e. ( `' S " { ( N ` w ) } ) <-> y S ( N ` w ) ) )
67 65 66 ax-mp 
 |-  ( y e. ( `' S " { ( N ` w ) } ) <-> y S ( N ` w ) )
68 60 64 67 3bitr4g 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( y e. ( `' R " { ( M ` w ) } ) <-> y e. ( `' S " { ( N ` w ) } ) ) )
69 68 eqrdv 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( `' R " { ( M ` w ) } ) = ( `' S " { ( N ` w ) } ) )
70 relinxp 
 |-  Rel ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) )
71 relinxp 
 |-  Rel ( S i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) )
72 vex 
 |-  z e. _V
73 72 eliniseg 
 |-  ( ( M ` w ) e. _V -> ( z e. ( `' R " { ( M ` w ) } ) <-> z R ( M ` w ) ) )
74 63 73 anbi12d 
 |-  ( ( M ` w ) e. _V -> ( ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) <-> ( y R ( M ` w ) /\ z R ( M ` w ) ) ) )
75 61 74 ax-mp 
 |-  ( ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) <-> ( y R ( M ` w ) /\ z R ( M ` w ) ) )
76 55 simprd 
 |-  ( ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) /\ y R ( M ` w ) ) -> ( z R ( M ` w ) -> ( y R z <-> y S z ) ) )
77 76 impr 
 |-  ( ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) /\ ( y R ( M ` w ) /\ z R ( M ` w ) ) ) -> ( y R z <-> y S z ) )
78 75 77 sylan2b 
 |-  ( ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) /\ ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) ) -> ( y R z <-> y S z ) )
79 78 pm5.32da 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( ( ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) /\ y R z ) <-> ( ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) /\ y S z ) ) )
80 df-br 
 |-  ( y ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) z <-> <. y , z >. e. ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) )
81 brinxp2 
 |-  ( y ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) z <-> ( ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) /\ y R z ) )
82 80 81 bitr3i 
 |-  ( <. y , z >. e. ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) <-> ( ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) /\ y R z ) )
83 df-br 
 |-  ( y ( S i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) z <-> <. y , z >. e. ( S i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) )
84 brinxp2 
 |-  ( y ( S i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) z <-> ( ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) /\ y S z ) )
85 83 84 bitr3i 
 |-  ( <. y , z >. e. ( S i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) <-> ( ( y e. ( `' R " { ( M ` w ) } ) /\ z e. ( `' R " { ( M ` w ) } ) ) /\ y S z ) )
86 79 82 85 3bitr4g 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( <. y , z >. e. ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) <-> <. y , z >. e. ( S i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) ) )
87 70 71 86 eqrelrdv 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) = ( S i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) )
88 69 sqxpeqd 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) = ( ( `' S " { ( N ` w ) } ) X. ( `' S " { ( N ` w ) } ) ) )
89 88 ineq2d 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( S i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) = ( S i^i ( ( `' S " { ( N ` w ) } ) X. ( `' S " { ( N ` w ) } ) ) ) )
90 87 89 eqtrd 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) = ( S i^i ( ( `' S " { ( N ` w ) } ) X. ( `' S " { ( N ` w ) } ) ) ) )
91 69 90 oveq12d 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( ( `' R " { ( M ` w ) } ) F ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) ) = ( ( `' S " { ( N ` w ) } ) F ( S i^i ( ( `' S " { ( N ` w ) } ) X. ( `' S " { ( N ` w ) } ) ) ) ) )
92 9 ffvelcdmi 
 |-  ( w e. dom M -> ( M ` w ) e. X )
93 92 adantl 
 |-  ( ( ph /\ w e. dom M ) -> ( M ` w ) e. X )
94 93 adantr 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( M ` w ) e. X )
95 1 2 4 fpwwe2lem3 
 |-  ( ( ph /\ ( M ` w ) e. X ) -> ( ( `' R " { ( M ` w ) } ) F ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) ) = ( M ` w ) )
96 47 94 95 syl2anc 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( ( `' R " { ( M ` w ) } ) F ( R i^i ( ( `' R " { ( M ` w ) } ) X. ( `' R " { ( M ` w ) } ) ) ) ) = ( M ` w ) )
97 12 ffvelcdmi 
 |-  ( w e. dom N -> ( N ` w ) e. Y )
98 52 97 syl 
 |-  ( ( ph /\ w e. dom M ) -> ( N ` w ) e. Y )
99 98 adantr 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( N ` w ) e. Y )
100 1 2 5 fpwwe2lem3 
 |-  ( ( ph /\ ( N ` w ) e. Y ) -> ( ( `' S " { ( N ` w ) } ) F ( S i^i ( ( `' S " { ( N ` w ) } ) X. ( `' S " { ( N ` w ) } ) ) ) ) = ( N ` w ) )
101 47 99 100 syl2anc 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( ( `' S " { ( N ` w ) } ) F ( S i^i ( ( `' S " { ( N ` w ) } ) X. ( `' S " { ( N ` w ) } ) ) ) ) = ( N ` w ) )
102 91 96 101 3eqtr3d 
 |-  ( ( ( ph /\ w e. dom M ) /\ ( M |` w ) = ( N |` w ) ) -> ( M ` w ) = ( N ` w ) )
103 102 ex 
 |-  ( ( ph /\ w e. dom M ) -> ( ( M |` w ) = ( N |` w ) -> ( M ` w ) = ( N ` w ) ) )
104 45 103 sylbird 
 |-  ( ( ph /\ w e. dom M ) -> ( A. y e. w ( M ` y ) = ( N ` y ) -> ( M ` w ) = ( N ` w ) ) )
105 32 104 syld 
 |-  ( ( ph /\ w e. dom M ) -> ( A. y e. w ( y e. dom M -> ( M ` y ) = ( N ` y ) ) -> ( M ` w ) = ( N ` w ) ) )
106 105 ex 
 |-  ( ph -> ( w e. dom M -> ( A. y e. w ( y e. dom M -> ( M ` y ) = ( N ` y ) ) -> ( M ` w ) = ( N ` w ) ) ) )
107 106 com23 
 |-  ( ph -> ( A. y e. w ( y e. dom M -> ( M ` y ) = ( N ` y ) ) -> ( w e. dom M -> ( M ` w ) = ( N ` w ) ) ) )
108 107 a2i 
 |-  ( ( ph -> A. y e. w ( y e. dom M -> ( M ` y ) = ( N ` y ) ) ) -> ( ph -> ( w e. dom M -> ( M ` w ) = ( N ` w ) ) ) )
109 25 108 sylbi 
 |-  ( A. y e. w ( ph -> ( y e. dom M -> ( M ` y ) = ( N ` y ) ) ) -> ( ph -> ( w e. dom M -> ( M ` w ) = ( N ` w ) ) ) )
110 109 a1i 
 |-  ( w e. On -> ( A. y e. w ( ph -> ( y e. dom M -> ( M ` y ) = ( N ` y ) ) ) -> ( ph -> ( w e. dom M -> ( M ` w ) = ( N ` w ) ) ) ) )
111 24 110 tfis2 
 |-  ( w e. On -> ( ph -> ( w e. dom M -> ( M ` w ) = ( N ` w ) ) ) )
112 111 com3l 
 |-  ( ph -> ( w e. dom M -> ( w e. On -> ( M ` w ) = ( N ` w ) ) ) )
113 18 112 mpdi 
 |-  ( ph -> ( w e. dom M -> ( M ` w ) = ( N ` w ) ) )
114 113 imp 
 |-  ( ( ph /\ w e. dom M ) -> ( M ` w ) = ( N ` w ) )
115 fvres 
 |-  ( w e. dom M -> ( ( N |` dom M ) ` w ) = ( N ` w ) )
116 115 adantl 
 |-  ( ( ph /\ w e. dom M ) -> ( ( N |` dom M ) ` w ) = ( N ` w ) )
117 114 116 eqtr4d 
 |-  ( ( ph /\ w e. dom M ) -> ( M ` w ) = ( ( N |` dom M ) ` w ) )
118 11 15 117 eqfnfvd 
 |-  ( ph -> M = ( N |` dom M ) )