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 |
1
|
relopabiv |
|- Rel W |
10 |
9
|
brrelex1i |
|- ( X W R -> X e. _V ) |
11 |
4 10
|
syl |
|- ( ph -> X e. _V ) |
12 |
1 2
|
fpwwe2lem2 |
|- ( ph -> ( X W 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 ) ) ) ) |
13 |
4 12
|
mpbid |
|- ( ph -> ( ( 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 ) ) ) |
14 |
13
|
simprld |
|- ( ph -> R We X ) |
15 |
6
|
oiiso |
|- ( ( X e. _V /\ R We X ) -> M Isom _E , R ( dom M , X ) ) |
16 |
11 14 15
|
syl2anc |
|- ( ph -> M Isom _E , R ( dom M , X ) ) |
17 |
|
isof1o |
|- ( M Isom _E , R ( dom M , X ) -> M : dom M -1-1-onto-> X ) |
18 |
|
f1ofo |
|- ( M : dom M -1-1-onto-> X -> M : dom M -onto-> X ) |
19 |
|
forn |
|- ( M : dom M -onto-> X -> ran M = X ) |
20 |
16 17 18 19
|
4syl |
|- ( ph -> ran M = X ) |
21 |
1 2 3 4 5 6 7 8
|
fpwwe2lem7 |
|- ( ph -> M = ( N |` dom M ) ) |
22 |
21
|
rneqd |
|- ( ph -> ran M = ran ( N |` dom M ) ) |
23 |
20 22
|
eqtr3d |
|- ( ph -> X = ran ( N |` dom M ) ) |
24 |
|
df-ima |
|- ( N " dom M ) = ran ( N |` dom M ) |
25 |
23 24
|
eqtr4di |
|- ( ph -> X = ( N " dom M ) ) |
26 |
|
imassrn |
|- ( N " dom M ) C_ ran N |
27 |
9
|
brrelex1i |
|- ( Y W S -> Y e. _V ) |
28 |
5 27
|
syl |
|- ( ph -> Y e. _V ) |
29 |
1 2
|
fpwwe2lem2 |
|- ( ph -> ( Y W S <-> ( ( Y C_ A /\ S C_ ( Y X. Y ) ) /\ ( S We Y /\ A. y e. Y [. ( `' S " { y } ) / u ]. ( u F ( S i^i ( u X. u ) ) ) = y ) ) ) ) |
30 |
5 29
|
mpbid |
|- ( ph -> ( ( Y C_ A /\ S C_ ( Y X. Y ) ) /\ ( S We Y /\ A. y e. Y [. ( `' S " { y } ) / u ]. ( u F ( S i^i ( u X. u ) ) ) = y ) ) ) |
31 |
30
|
simprld |
|- ( ph -> S We Y ) |
32 |
7
|
oiiso |
|- ( ( Y e. _V /\ S We Y ) -> N Isom _E , S ( dom N , Y ) ) |
33 |
28 31 32
|
syl2anc |
|- ( ph -> N Isom _E , S ( dom N , Y ) ) |
34 |
|
isof1o |
|- ( N Isom _E , S ( dom N , Y ) -> N : dom N -1-1-onto-> Y ) |
35 |
|
f1ofo |
|- ( N : dom N -1-1-onto-> Y -> N : dom N -onto-> Y ) |
36 |
|
forn |
|- ( N : dom N -onto-> Y -> ran N = Y ) |
37 |
33 34 35 36
|
4syl |
|- ( ph -> ran N = Y ) |
38 |
26 37
|
sseqtrid |
|- ( ph -> ( N " dom M ) C_ Y ) |
39 |
25 38
|
eqsstrd |
|- ( ph -> X C_ Y ) |
40 |
13
|
simplrd |
|- ( ph -> R C_ ( X X. X ) ) |
41 |
|
relxp |
|- Rel ( X X. X ) |
42 |
|
relss |
|- ( R C_ ( X X. X ) -> ( Rel ( X X. X ) -> Rel R ) ) |
43 |
40 41 42
|
mpisyl |
|- ( ph -> Rel R ) |
44 |
|
relinxp |
|- Rel ( S i^i ( Y X. X ) ) |
45 |
43 44
|
jctir |
|- ( ph -> ( Rel R /\ Rel ( S i^i ( Y X. X ) ) ) ) |
46 |
40
|
ssbrd |
|- ( ph -> ( x R y -> x ( X X. X ) y ) ) |
47 |
|
brxp |
|- ( x ( X X. X ) y <-> ( x e. X /\ y e. X ) ) |
48 |
46 47
|
imbitrdi |
|- ( ph -> ( x R y -> ( x e. X /\ y e. X ) ) ) |
49 |
|
brinxp2 |
|- ( x ( S i^i ( Y X. X ) ) y <-> ( ( x e. Y /\ y e. X ) /\ x S y ) ) |
50 |
|
isocnv |
|- ( N Isom _E , S ( dom N , Y ) -> `' N Isom S , _E ( Y , dom N ) ) |
51 |
33 50
|
syl |
|- ( ph -> `' N Isom S , _E ( Y , dom N ) ) |
52 |
51
|
adantr |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' N Isom S , _E ( Y , dom N ) ) |
53 |
|
isof1o |
|- ( `' N Isom S , _E ( Y , dom N ) -> `' N : Y -1-1-onto-> dom N ) |
54 |
|
f1ofn |
|- ( `' N : Y -1-1-onto-> dom N -> `' N Fn Y ) |
55 |
52 53 54
|
3syl |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' N Fn Y ) |
56 |
|
simprll |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> x e. Y ) |
57 |
|
simprr |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> x S y ) |
58 |
39
|
adantr |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> X C_ Y ) |
59 |
|
simprlr |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> y e. X ) |
60 |
58 59
|
sseldd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> y e. Y ) |
61 |
|
isorel |
|- ( ( `' N Isom S , _E ( Y , dom N ) /\ ( x e. Y /\ y e. Y ) ) -> ( x S y <-> ( `' N ` x ) _E ( `' N ` y ) ) ) |
62 |
52 56 60 61
|
syl12anc |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( x S y <-> ( `' N ` x ) _E ( `' N ` y ) ) ) |
63 |
57 62
|
mpbid |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' N ` x ) _E ( `' N ` y ) ) |
64 |
|
fvex |
|- ( `' N ` y ) e. _V |
65 |
64
|
epeli |
|- ( ( `' N ` x ) _E ( `' N ` y ) <-> ( `' N ` x ) e. ( `' N ` y ) ) |
66 |
63 65
|
sylib |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' N ` x ) e. ( `' N ` y ) ) |
67 |
21
|
adantr |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> M = ( N |` dom M ) ) |
68 |
67
|
cnveqd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' M = `' ( N |` dom M ) ) |
69 |
|
fnfun |
|- ( `' N Fn Y -> Fun `' N ) |
70 |
|
funcnvres |
|- ( Fun `' N -> `' ( N |` dom M ) = ( `' N |` ( N " dom M ) ) ) |
71 |
55 69 70
|
3syl |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' ( N |` dom M ) = ( `' N |` ( N " dom M ) ) ) |
72 |
68 71
|
eqtrd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' M = ( `' N |` ( N " dom M ) ) ) |
73 |
72
|
fveq1d |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' M ` y ) = ( ( `' N |` ( N " dom M ) ) ` y ) ) |
74 |
25
|
adantr |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> X = ( N " dom M ) ) |
75 |
59 74
|
eleqtrd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> y e. ( N " dom M ) ) |
76 |
75
|
fvresd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( ( `' N |` ( N " dom M ) ) ` y ) = ( `' N ` y ) ) |
77 |
73 76
|
eqtrd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' M ` y ) = ( `' N ` y ) ) |
78 |
|
isocnv |
|- ( M Isom _E , R ( dom M , X ) -> `' M Isom R , _E ( X , dom M ) ) |
79 |
|
isof1o |
|- ( `' M Isom R , _E ( X , dom M ) -> `' M : X -1-1-onto-> dom M ) |
80 |
|
f1of |
|- ( `' M : X -1-1-onto-> dom M -> `' M : X --> dom M ) |
81 |
16 78 79 80
|
4syl |
|- ( ph -> `' M : X --> dom M ) |
82 |
81
|
adantr |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> `' M : X --> dom M ) |
83 |
82 59
|
ffvelcdmd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' M ` y ) e. dom M ) |
84 |
77 83
|
eqeltrrd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' N ` y ) e. dom M ) |
85 |
6
|
oicl |
|- Ord dom M |
86 |
|
ordtr1 |
|- ( Ord dom M -> ( ( ( `' N ` x ) e. ( `' N ` y ) /\ ( `' N ` y ) e. dom M ) -> ( `' N ` x ) e. dom M ) ) |
87 |
85 86
|
ax-mp |
|- ( ( ( `' N ` x ) e. ( `' N ` y ) /\ ( `' N ` y ) e. dom M ) -> ( `' N ` x ) e. dom M ) |
88 |
66 84 87
|
syl2anc |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( `' N ` x ) e. dom M ) |
89 |
55 56 88
|
elpreimad |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> x e. ( `' `' N " dom M ) ) |
90 |
|
imacnvcnv |
|- ( `' `' N " dom M ) = ( N " dom M ) |
91 |
74 90
|
eqtr4di |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> X = ( `' `' N " dom M ) ) |
92 |
89 91
|
eleqtrrd |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> x e. X ) |
93 |
92 59
|
jca |
|- ( ( ph /\ ( ( x e. Y /\ y e. X ) /\ x S y ) ) -> ( x e. X /\ y e. X ) ) |
94 |
93
|
ex |
|- ( ph -> ( ( ( x e. Y /\ y e. X ) /\ x S y ) -> ( x e. X /\ y e. X ) ) ) |
95 |
49 94
|
biimtrid |
|- ( ph -> ( x ( S i^i ( Y X. X ) ) y -> ( x e. X /\ y e. X ) ) ) |
96 |
21
|
adantr |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> M = ( N |` dom M ) ) |
97 |
96
|
cnveqd |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> `' M = `' ( N |` dom M ) ) |
98 |
97
|
fveq1d |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( `' M ` x ) = ( `' ( N |` dom M ) ` x ) ) |
99 |
97
|
fveq1d |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( `' M ` y ) = ( `' ( N |` dom M ) ` y ) ) |
100 |
98 99
|
breq12d |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( `' M ` x ) _E ( `' M ` y ) <-> ( `' ( N |` dom M ) ` x ) _E ( `' ( N |` dom M ) ` y ) ) ) |
101 |
16 78
|
syl |
|- ( ph -> `' M Isom R , _E ( X , dom M ) ) |
102 |
|
isorel |
|- ( ( `' M Isom R , _E ( X , dom M ) /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> ( `' M ` x ) _E ( `' M ` y ) ) ) |
103 |
101 102
|
sylan |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> ( `' M ` x ) _E ( `' M ` y ) ) ) |
104 |
|
eqidd |
|- ( ph -> ( N " dom M ) = ( N " dom M ) ) |
105 |
|
isores3 |
|- ( ( N Isom _E , S ( dom N , Y ) /\ dom M C_ dom N /\ ( N " dom M ) = ( N " dom M ) ) -> ( N |` dom M ) Isom _E , S ( dom M , ( N " dom M ) ) ) |
106 |
33 8 104 105
|
syl3anc |
|- ( ph -> ( N |` dom M ) Isom _E , S ( dom M , ( N " dom M ) ) ) |
107 |
|
isocnv |
|- ( ( N |` dom M ) Isom _E , S ( dom M , ( N " dom M ) ) -> `' ( N |` dom M ) Isom S , _E ( ( N " dom M ) , dom M ) ) |
108 |
106 107
|
syl |
|- ( ph -> `' ( N |` dom M ) Isom S , _E ( ( N " dom M ) , dom M ) ) |
109 |
108
|
adantr |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> `' ( N |` dom M ) Isom S , _E ( ( N " dom M ) , dom M ) ) |
110 |
|
simprl |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> x e. X ) |
111 |
25
|
adantr |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> X = ( N " dom M ) ) |
112 |
110 111
|
eleqtrd |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> x e. ( N " dom M ) ) |
113 |
|
simprr |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> y e. X ) |
114 |
113 111
|
eleqtrd |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> y e. ( N " dom M ) ) |
115 |
|
isorel |
|- ( ( `' ( N |` dom M ) Isom S , _E ( ( N " dom M ) , dom M ) /\ ( x e. ( N " dom M ) /\ y e. ( N " dom M ) ) ) -> ( x S y <-> ( `' ( N |` dom M ) ` x ) _E ( `' ( N |` dom M ) ` y ) ) ) |
116 |
109 112 114 115
|
syl12anc |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x S y <-> ( `' ( N |` dom M ) ` x ) _E ( `' ( N |` dom M ) ` y ) ) ) |
117 |
100 103 116
|
3bitr4d |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> x S y ) ) |
118 |
39
|
sselda |
|- ( ( ph /\ x e. X ) -> x e. Y ) |
119 |
118
|
adantrr |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> x e. Y ) |
120 |
119 113
|
jca |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x e. Y /\ y e. X ) ) |
121 |
120
|
biantrurd |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x S y <-> ( ( x e. Y /\ y e. X ) /\ x S y ) ) ) |
122 |
121 49
|
bitr4di |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x S y <-> x ( S i^i ( Y X. X ) ) y ) ) |
123 |
117 122
|
bitrd |
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x R y <-> x ( S i^i ( Y X. X ) ) y ) ) |
124 |
123
|
ex |
|- ( ph -> ( ( x e. X /\ y e. X ) -> ( x R y <-> x ( S i^i ( Y X. X ) ) y ) ) ) |
125 |
48 95 124
|
pm5.21ndd |
|- ( ph -> ( x R y <-> x ( S i^i ( Y X. X ) ) y ) ) |
126 |
|
df-br |
|- ( x R y <-> <. x , y >. e. R ) |
127 |
|
df-br |
|- ( x ( S i^i ( Y X. X ) ) y <-> <. x , y >. e. ( S i^i ( Y X. X ) ) ) |
128 |
125 126 127
|
3bitr3g |
|- ( ph -> ( <. x , y >. e. R <-> <. x , y >. e. ( S i^i ( Y X. X ) ) ) ) |
129 |
128
|
eqrelrdv2 |
|- ( ( ( Rel R /\ Rel ( S i^i ( Y X. X ) ) ) /\ ph ) -> R = ( S i^i ( Y X. X ) ) ) |
130 |
45 129
|
mpancom |
|- ( ph -> R = ( S i^i ( Y X. X ) ) ) |
131 |
39 130
|
jca |
|- ( ph -> ( X C_ Y /\ R = ( S i^i ( Y X. X ) ) ) ) |