Step |
Hyp |
Ref |
Expression |
1 |
|
wemapso.t |
|- T = { <. x , y >. | E. z e. A ( ( x ` z ) S ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } |
2 |
|
wemaplem2.p |
|- ( ph -> P e. ( B ^m A ) ) |
3 |
|
wemaplem2.x |
|- ( ph -> X e. ( B ^m A ) ) |
4 |
|
wemaplem2.q |
|- ( ph -> Q e. ( B ^m A ) ) |
5 |
|
wemaplem2.r |
|- ( ph -> R Or A ) |
6 |
|
wemaplem2.s |
|- ( ph -> S Po B ) |
7 |
|
wemaplem2.px1 |
|- ( ph -> a e. A ) |
8 |
|
wemaplem2.px2 |
|- ( ph -> ( P ` a ) S ( X ` a ) ) |
9 |
|
wemaplem2.px3 |
|- ( ph -> A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) ) |
10 |
|
wemaplem2.xq1 |
|- ( ph -> b e. A ) |
11 |
|
wemaplem2.xq2 |
|- ( ph -> ( X ` b ) S ( Q ` b ) ) |
12 |
|
wemaplem2.xq3 |
|- ( ph -> A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) |
13 |
7 10
|
ifcld |
|- ( ph -> if ( a R b , a , b ) e. A ) |
14 |
8
|
adantr |
|- ( ( ph /\ a R b ) -> ( P ` a ) S ( X ` a ) ) |
15 |
|
breq1 |
|- ( c = a -> ( c R b <-> a R b ) ) |
16 |
|
fveq2 |
|- ( c = a -> ( X ` c ) = ( X ` a ) ) |
17 |
|
fveq2 |
|- ( c = a -> ( Q ` c ) = ( Q ` a ) ) |
18 |
16 17
|
eqeq12d |
|- ( c = a -> ( ( X ` c ) = ( Q ` c ) <-> ( X ` a ) = ( Q ` a ) ) ) |
19 |
15 18
|
imbi12d |
|- ( c = a -> ( ( c R b -> ( X ` c ) = ( Q ` c ) ) <-> ( a R b -> ( X ` a ) = ( Q ` a ) ) ) ) |
20 |
19 12 7
|
rspcdva |
|- ( ph -> ( a R b -> ( X ` a ) = ( Q ` a ) ) ) |
21 |
20
|
imp |
|- ( ( ph /\ a R b ) -> ( X ` a ) = ( Q ` a ) ) |
22 |
14 21
|
breqtrd |
|- ( ( ph /\ a R b ) -> ( P ` a ) S ( Q ` a ) ) |
23 |
|
iftrue |
|- ( a R b -> if ( a R b , a , b ) = a ) |
24 |
23
|
fveq2d |
|- ( a R b -> ( P ` if ( a R b , a , b ) ) = ( P ` a ) ) |
25 |
23
|
fveq2d |
|- ( a R b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` a ) ) |
26 |
24 25
|
breq12d |
|- ( a R b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` a ) S ( Q ` a ) ) ) |
27 |
26
|
adantl |
|- ( ( ph /\ a R b ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` a ) S ( Q ` a ) ) ) |
28 |
22 27
|
mpbird |
|- ( ( ph /\ a R b ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) ) |
29 |
6
|
adantr |
|- ( ( ph /\ a = b ) -> S Po B ) |
30 |
|
elmapi |
|- ( P e. ( B ^m A ) -> P : A --> B ) |
31 |
2 30
|
syl |
|- ( ph -> P : A --> B ) |
32 |
31 10
|
ffvelrnd |
|- ( ph -> ( P ` b ) e. B ) |
33 |
|
elmapi |
|- ( X e. ( B ^m A ) -> X : A --> B ) |
34 |
3 33
|
syl |
|- ( ph -> X : A --> B ) |
35 |
34 10
|
ffvelrnd |
|- ( ph -> ( X ` b ) e. B ) |
36 |
|
elmapi |
|- ( Q e. ( B ^m A ) -> Q : A --> B ) |
37 |
4 36
|
syl |
|- ( ph -> Q : A --> B ) |
38 |
37 10
|
ffvelrnd |
|- ( ph -> ( Q ` b ) e. B ) |
39 |
32 35 38
|
3jca |
|- ( ph -> ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) ) |
40 |
39
|
adantr |
|- ( ( ph /\ a = b ) -> ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) ) |
41 |
|
fveq2 |
|- ( a = b -> ( P ` a ) = ( P ` b ) ) |
42 |
|
fveq2 |
|- ( a = b -> ( X ` a ) = ( X ` b ) ) |
43 |
41 42
|
breq12d |
|- ( a = b -> ( ( P ` a ) S ( X ` a ) <-> ( P ` b ) S ( X ` b ) ) ) |
44 |
8 43
|
syl5ibcom |
|- ( ph -> ( a = b -> ( P ` b ) S ( X ` b ) ) ) |
45 |
44
|
imp |
|- ( ( ph /\ a = b ) -> ( P ` b ) S ( X ` b ) ) |
46 |
11
|
adantr |
|- ( ( ph /\ a = b ) -> ( X ` b ) S ( Q ` b ) ) |
47 |
|
potr |
|- ( ( S Po B /\ ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) ) -> ( ( ( P ` b ) S ( X ` b ) /\ ( X ` b ) S ( Q ` b ) ) -> ( P ` b ) S ( Q ` b ) ) ) |
48 |
47
|
imp |
|- ( ( ( S Po B /\ ( ( P ` b ) e. B /\ ( X ` b ) e. B /\ ( Q ` b ) e. B ) ) /\ ( ( P ` b ) S ( X ` b ) /\ ( X ` b ) S ( Q ` b ) ) ) -> ( P ` b ) S ( Q ` b ) ) |
49 |
29 40 45 46 48
|
syl22anc |
|- ( ( ph /\ a = b ) -> ( P ` b ) S ( Q ` b ) ) |
50 |
|
ifeq1 |
|- ( a = b -> if ( a R b , a , b ) = if ( a R b , b , b ) ) |
51 |
|
ifid |
|- if ( a R b , b , b ) = b |
52 |
50 51
|
eqtrdi |
|- ( a = b -> if ( a R b , a , b ) = b ) |
53 |
52
|
fveq2d |
|- ( a = b -> ( P ` if ( a R b , a , b ) ) = ( P ` b ) ) |
54 |
52
|
fveq2d |
|- ( a = b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` b ) ) |
55 |
53 54
|
breq12d |
|- ( a = b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) ) |
56 |
55
|
adantl |
|- ( ( ph /\ a = b ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) ) |
57 |
49 56
|
mpbird |
|- ( ( ph /\ a = b ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) ) |
58 |
|
breq1 |
|- ( c = b -> ( c R a <-> b R a ) ) |
59 |
|
fveq2 |
|- ( c = b -> ( P ` c ) = ( P ` b ) ) |
60 |
|
fveq2 |
|- ( c = b -> ( X ` c ) = ( X ` b ) ) |
61 |
59 60
|
eqeq12d |
|- ( c = b -> ( ( P ` c ) = ( X ` c ) <-> ( P ` b ) = ( X ` b ) ) ) |
62 |
58 61
|
imbi12d |
|- ( c = b -> ( ( c R a -> ( P ` c ) = ( X ` c ) ) <-> ( b R a -> ( P ` b ) = ( X ` b ) ) ) ) |
63 |
62 9 10
|
rspcdva |
|- ( ph -> ( b R a -> ( P ` b ) = ( X ` b ) ) ) |
64 |
63
|
imp |
|- ( ( ph /\ b R a ) -> ( P ` b ) = ( X ` b ) ) |
65 |
11
|
adantr |
|- ( ( ph /\ b R a ) -> ( X ` b ) S ( Q ` b ) ) |
66 |
64 65
|
eqbrtrd |
|- ( ( ph /\ b R a ) -> ( P ` b ) S ( Q ` b ) ) |
67 |
|
sopo |
|- ( R Or A -> R Po A ) |
68 |
5 67
|
syl |
|- ( ph -> R Po A ) |
69 |
|
po2nr |
|- ( ( R Po A /\ ( b e. A /\ a e. A ) ) -> -. ( b R a /\ a R b ) ) |
70 |
68 10 7 69
|
syl12anc |
|- ( ph -> -. ( b R a /\ a R b ) ) |
71 |
|
nan |
|- ( ( ph -> -. ( b R a /\ a R b ) ) <-> ( ( ph /\ b R a ) -> -. a R b ) ) |
72 |
70 71
|
mpbi |
|- ( ( ph /\ b R a ) -> -. a R b ) |
73 |
|
iffalse |
|- ( -. a R b -> if ( a R b , a , b ) = b ) |
74 |
73
|
fveq2d |
|- ( -. a R b -> ( P ` if ( a R b , a , b ) ) = ( P ` b ) ) |
75 |
73
|
fveq2d |
|- ( -. a R b -> ( Q ` if ( a R b , a , b ) ) = ( Q ` b ) ) |
76 |
74 75
|
breq12d |
|- ( -. a R b -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) ) |
77 |
72 76
|
syl |
|- ( ( ph /\ b R a ) -> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) <-> ( P ` b ) S ( Q ` b ) ) ) |
78 |
66 77
|
mpbird |
|- ( ( ph /\ b R a ) -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) ) |
79 |
|
solin |
|- ( ( R Or A /\ ( a e. A /\ b e. A ) ) -> ( a R b \/ a = b \/ b R a ) ) |
80 |
5 7 10 79
|
syl12anc |
|- ( ph -> ( a R b \/ a = b \/ b R a ) ) |
81 |
28 57 78 80
|
mpjao3dan |
|- ( ph -> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) ) |
82 |
|
r19.26 |
|- ( A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) <-> ( A. c e. A ( c R a -> ( P ` c ) = ( X ` c ) ) /\ A. c e. A ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) |
83 |
9 12 82
|
sylanbrc |
|- ( ph -> A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) ) |
84 |
5 7 10
|
3jca |
|- ( ph -> ( R Or A /\ a e. A /\ b e. A ) ) |
85 |
|
anim12 |
|- ( ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> ( ( c R a /\ c R b ) -> ( ( P ` c ) = ( X ` c ) /\ ( X ` c ) = ( Q ` c ) ) ) ) |
86 |
|
eqtr |
|- ( ( ( P ` c ) = ( X ` c ) /\ ( X ` c ) = ( Q ` c ) ) -> ( P ` c ) = ( Q ` c ) ) |
87 |
85 86
|
syl6 |
|- ( ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) ) |
88 |
87
|
ralimi |
|- ( A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> A. c e. A ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) ) |
89 |
|
simpl1 |
|- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> R Or A ) |
90 |
|
simpr |
|- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> c e. A ) |
91 |
|
simpl2 |
|- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> a e. A ) |
92 |
|
simpl3 |
|- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> b e. A ) |
93 |
|
soltmin |
|- ( ( R Or A /\ ( c e. A /\ a e. A /\ b e. A ) ) -> ( c R if ( a R b , a , b ) <-> ( c R a /\ c R b ) ) ) |
94 |
89 90 91 92 93
|
syl13anc |
|- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> ( c R if ( a R b , a , b ) <-> ( c R a /\ c R b ) ) ) |
95 |
94
|
biimpd |
|- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> ( c R if ( a R b , a , b ) -> ( c R a /\ c R b ) ) ) |
96 |
95
|
imim1d |
|- ( ( ( R Or A /\ a e. A /\ b e. A ) /\ c e. A ) -> ( ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) -> ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) |
97 |
96
|
ralimdva |
|- ( ( R Or A /\ a e. A /\ b e. A ) -> ( A. c e. A ( ( c R a /\ c R b ) -> ( P ` c ) = ( Q ` c ) ) -> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) |
98 |
84 88 97
|
syl2im |
|- ( ph -> ( A. c e. A ( ( c R a -> ( P ` c ) = ( X ` c ) ) /\ ( c R b -> ( X ` c ) = ( Q ` c ) ) ) -> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) |
99 |
83 98
|
mpd |
|- ( ph -> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) |
100 |
|
fveq2 |
|- ( d = if ( a R b , a , b ) -> ( P ` d ) = ( P ` if ( a R b , a , b ) ) ) |
101 |
|
fveq2 |
|- ( d = if ( a R b , a , b ) -> ( Q ` d ) = ( Q ` if ( a R b , a , b ) ) ) |
102 |
100 101
|
breq12d |
|- ( d = if ( a R b , a , b ) -> ( ( P ` d ) S ( Q ` d ) <-> ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) ) ) |
103 |
|
breq2 |
|- ( d = if ( a R b , a , b ) -> ( c R d <-> c R if ( a R b , a , b ) ) ) |
104 |
103
|
imbi1d |
|- ( d = if ( a R b , a , b ) -> ( ( c R d -> ( P ` c ) = ( Q ` c ) ) <-> ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) |
105 |
104
|
ralbidv |
|- ( d = if ( a R b , a , b ) -> ( A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) <-> A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) |
106 |
102 105
|
anbi12d |
|- ( d = if ( a R b , a , b ) -> ( ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) <-> ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) /\ A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) ) |
107 |
106
|
rspcev |
|- ( ( if ( a R b , a , b ) e. A /\ ( ( P ` if ( a R b , a , b ) ) S ( Q ` if ( a R b , a , b ) ) /\ A. c e. A ( c R if ( a R b , a , b ) -> ( P ` c ) = ( Q ` c ) ) ) ) -> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) ) |
108 |
13 81 99 107
|
syl12anc |
|- ( ph -> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) ) |
109 |
1
|
wemaplem1 |
|- ( ( P e. ( B ^m A ) /\ Q e. ( B ^m A ) ) -> ( P T Q <-> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) ) ) |
110 |
2 4 109
|
syl2anc |
|- ( ph -> ( P T Q <-> E. d e. A ( ( P ` d ) S ( Q ` d ) /\ A. c e. A ( c R d -> ( P ` c ) = ( Q ` c ) ) ) ) ) |
111 |
108 110
|
mpbird |
|- ( ph -> P T Q ) |