Metamath Proof Explorer

Theorem wemapsolem

Description: Lemma for wemapso . (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Mario Carneiro, 8-Feb-2015) (Revised by AV, 21-Jul-2024)

Ref Expression
Hypotheses 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 ) ) ) }
wemapsolem.1 
|- U C_ ( B ^m A )
wemapsolem.2 
|- ( ph -> R Or A )
wemapsolem.3 
|- ( ph -> S Or B )
wemapsolem.4 
|- ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> E. c e. dom ( a \ b ) A. d e. dom ( a \ b ) -. d R c )
Assertion wemapsolem 
|- ( ph -> T Or U )

Proof

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 wemapsolem.1 
 |-  U C_ ( B ^m A )
3 wemapsolem.2 
 |-  ( ph -> R Or A )
4 wemapsolem.3 
 |-  ( ph -> S Or B )
5 wemapsolem.4 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> E. c e. dom ( a \ b ) A. d e. dom ( a \ b ) -. d R c )
6 sopo 
 |-  ( S Or B -> S Po B )
7 4 6 syl 
 |-  ( ph -> S Po B )
8 1 wemappo 
 |-  ( ( R Or A /\ S Po B ) -> T Po ( B ^m A ) )
9 3 7 8 syl2anc 
 |-  ( ph -> T Po ( B ^m A ) )
10 poss 
 |-  ( U C_ ( B ^m A ) -> ( T Po ( B ^m A ) -> T Po U ) )
11 2 9 10 mpsyl 
 |-  ( ph -> T Po U )
12 df-ne 
 |-  ( a =/= b <-> -. a = b )
13 simprll 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a e. U )
14 2 13 sselid 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a e. ( B ^m A ) )
15 elmapi 
 |-  ( a e. ( B ^m A ) -> a : A --> B )
16 14 15 syl 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a : A --> B )
17 16 ffnd 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> a Fn A )
18 simprlr 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b e. U )
19 2 18 sselid 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b e. ( B ^m A ) )
20 elmapi 
 |-  ( b e. ( B ^m A ) -> b : A --> B )
21 19 20 syl 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b : A --> B )
22 21 ffnd 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> b Fn A )
23 fndmdif 
 |-  ( ( a Fn A /\ b Fn A ) -> dom ( a \ b ) = { x e. A | ( a ` x ) =/= ( b ` x ) } )
24 17 22 23 syl2anc 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> dom ( a \ b ) = { x e. A | ( a ` x ) =/= ( b ` x ) } )
25 24 eleq2d 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( c e. dom ( a \ b ) <-> c e. { x e. A | ( a ` x ) =/= ( b ` x ) } ) )
26 nesym 
 |-  ( ( a ` x ) =/= ( b ` x ) <-> -. ( b ` x ) = ( a ` x ) )
27 fveq2 
 |-  ( x = c -> ( b ` x ) = ( b ` c ) )
28 fveq2 
 |-  ( x = c -> ( a ` x ) = ( a ` c ) )
29 27 28 eqeq12d 
 |-  ( x = c -> ( ( b ` x ) = ( a ` x ) <-> ( b ` c ) = ( a ` c ) ) )
30 29 notbid 
 |-  ( x = c -> ( -. ( b ` x ) = ( a ` x ) <-> -. ( b ` c ) = ( a ` c ) ) )
31 26 30 bitrid 
 |-  ( x = c -> ( ( a ` x ) =/= ( b ` x ) <-> -. ( b ` c ) = ( a ` c ) ) )
32 31 elrab 
 |-  ( c e. { x e. A | ( a ` x ) =/= ( b ` x ) } <-> ( c e. A /\ -. ( b ` c ) = ( a ` c ) ) )
33 25 32 bitrdi 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( c e. dom ( a \ b ) <-> ( c e. A /\ -. ( b ` c ) = ( a ` c ) ) ) )
34 24 eleq2d 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( d e. dom ( a \ b ) <-> d e. { x e. A | ( a ` x ) =/= ( b ` x ) } ) )
35 fveq2 
 |-  ( x = d -> ( b ` x ) = ( b ` d ) )
36 fveq2 
 |-  ( x = d -> ( a ` x ) = ( a ` d ) )
37 35 36 eqeq12d 
 |-  ( x = d -> ( ( b ` x ) = ( a ` x ) <-> ( b ` d ) = ( a ` d ) ) )
38 37 notbid 
 |-  ( x = d -> ( -. ( b ` x ) = ( a ` x ) <-> -. ( b ` d ) = ( a ` d ) ) )
39 26 38 bitrid 
 |-  ( x = d -> ( ( a ` x ) =/= ( b ` x ) <-> -. ( b ` d ) = ( a ` d ) ) )
40 39 elrab 
 |-  ( d e. { x e. A | ( a ` x ) =/= ( b ` x ) } <-> ( d e. A /\ -. ( b ` d ) = ( a ` d ) ) )
41 34 40 bitrdi 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( d e. dom ( a \ b ) <-> ( d e. A /\ -. ( b ` d ) = ( a ` d ) ) ) )
42 41 imbi1d 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( ( d e. dom ( a \ b ) -> -. d R c ) <-> ( ( d e. A /\ -. ( b ` d ) = ( a ` d ) ) -> -. d R c ) ) )
43 impexp 
 |-  ( ( ( d e. A /\ -. ( b ` d ) = ( a ` d ) ) -> -. d R c ) <-> ( d e. A -> ( -. ( b ` d ) = ( a ` d ) -> -. d R c ) ) )
44 con34b 
 |-  ( ( d R c -> ( b ` d ) = ( a ` d ) ) <-> ( -. ( b ` d ) = ( a ` d ) -> -. d R c ) )
45 44 imbi2i 
 |-  ( ( d e. A -> ( d R c -> ( b ` d ) = ( a ` d ) ) ) <-> ( d e. A -> ( -. ( b ` d ) = ( a ` d ) -> -. d R c ) ) )
46 43 45 bitr4i 
 |-  ( ( ( d e. A /\ -. ( b ` d ) = ( a ` d ) ) -> -. d R c ) <-> ( d e. A -> ( d R c -> ( b ` d ) = ( a ` d ) ) ) )
47 42 46 bitrdi 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( ( d e. dom ( a \ b ) -> -. d R c ) <-> ( d e. A -> ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) )
48 47 ralbidv2 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( A. d e. dom ( a \ b ) -. d R c <-> A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) )
49 33 48 anbi12d 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( ( c e. dom ( a \ b ) /\ A. d e. dom ( a \ b ) -. d R c ) <-> ( ( c e. A /\ -. ( b ` c ) = ( a ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) )
50 anass 
 |-  ( ( ( c e. A /\ -. ( b ` c ) = ( a ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) <-> ( c e. A /\ ( -. ( b ` c ) = ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) )
51 49 50 bitrdi 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( ( c e. dom ( a \ b ) /\ A. d e. dom ( a \ b ) -. d R c ) <-> ( c e. A /\ ( -. ( b ` c ) = ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) ) )
52 51 rexbidv2 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( E. c e. dom ( a \ b ) A. d e. dom ( a \ b ) -. d R c <-> E. c e. A ( -. ( b ` c ) = ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) )
53 5 52 mpbid 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> E. c e. A ( -. ( b ` c ) = ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) )
54 4 ad2antrr 
 |-  ( ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> S Or B )
55 21 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( b ` c ) e. B )
56 16 ffvelcdmda 
 |-  ( ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( a ` c ) e. B )
57 sotrieq 
 |-  ( ( S Or B /\ ( ( b ` c ) e. B /\ ( a ` c ) e. B ) ) -> ( ( b ` c ) = ( a ` c ) <-> -. ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) ) )
58 57 con2bid 
 |-  ( ( S Or B /\ ( ( b ` c ) e. B /\ ( a ` c ) e. B ) ) -> ( ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) <-> -. ( b ` c ) = ( a ` c ) ) )
59 58 biimprd 
 |-  ( ( S Or B /\ ( ( b ` c ) e. B /\ ( a ` c ) e. B ) ) -> ( -. ( b ` c ) = ( a ` c ) -> ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) ) )
60 54 55 56 59 syl12anc 
 |-  ( ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( -. ( b ` c ) = ( a ` c ) -> ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) ) )
61 60 anim1d 
 |-  ( ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) /\ c e. A ) -> ( ( -. ( b ` c ) = ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) -> ( ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) )
62 61 reximdva 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( E. c e. A ( -. ( b ` c ) = ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) -> E. c e. A ( ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) )
63 53 62 mpd 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> E. c e. A ( ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) )
64 1 wemaplem1 
 |-  ( ( b e. _V /\ a e. _V ) -> ( b T a <-> E. c e. A ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) )
65 64 el2v 
 |-  ( b T a <-> E. c e. A ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) )
66 1 wemaplem1 
 |-  ( ( a e. _V /\ b e. _V ) -> ( a T b <-> E. c e. A ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) ) )
67 66 el2v 
 |-  ( a T b <-> E. c e. A ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) )
68 65 67 orbi12i 
 |-  ( ( b T a \/ a T b ) <-> ( E. c e. A ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) \/ E. c e. A ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) ) )
69 r19.43 
 |-  ( E. c e. A ( ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) \/ ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) ) <-> ( E. c e. A ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) \/ E. c e. A ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) ) )
70 andir 
 |-  ( ( ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) <-> ( ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) \/ ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) )
71 eqcom 
 |-  ( ( b ` d ) = ( a ` d ) <-> ( a ` d ) = ( b ` d ) )
72 71 imbi2i 
 |-  ( ( d R c -> ( b ` d ) = ( a ` d ) ) <-> ( d R c -> ( a ` d ) = ( b ` d ) ) )
73 72 ralbii 
 |-  ( A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) <-> A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) )
74 73 anbi2i 
 |-  ( ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) <-> ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) )
75 74 orbi2i 
 |-  ( ( ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) \/ ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) ) <-> ( ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) \/ ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) ) )
76 70 75 bitr2i 
 |-  ( ( ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) \/ ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) ) <-> ( ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) )
77 76 rexbii 
 |-  ( E. c e. A ( ( ( b ` c ) S ( a ` c ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) \/ ( ( a ` c ) S ( b ` c ) /\ A. d e. A ( d R c -> ( a ` d ) = ( b ` d ) ) ) ) <-> E. c e. A ( ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) )
78 68 69 77 3bitr2i 
 |-  ( ( b T a \/ a T b ) <-> E. c e. A ( ( ( b ` c ) S ( a ` c ) \/ ( a ` c ) S ( b ` c ) ) /\ A. d e. A ( d R c -> ( b ` d ) = ( a ` d ) ) ) )
79 63 78 sylibr 
 |-  ( ( ph /\ ( ( a e. U /\ b e. U ) /\ a =/= b ) ) -> ( b T a \/ a T b ) )
80 79 expr 
 |-  ( ( ph /\ ( a e. U /\ b e. U ) ) -> ( a =/= b -> ( b T a \/ a T b ) ) )
81 12 80 biimtrrid 
 |-  ( ( ph /\ ( a e. U /\ b e. U ) ) -> ( -. a = b -> ( b T a \/ a T b ) ) )
82 81 orrd 
 |-  ( ( ph /\ ( a e. U /\ b e. U ) ) -> ( a = b \/ ( b T a \/ a T b ) ) )
83 3orrot 
 |-  ( ( a T b \/ a = b \/ b T a ) <-> ( a = b \/ b T a \/ a T b ) )
84 3orass 
 |-  ( ( a = b \/ b T a \/ a T b ) <-> ( a = b \/ ( b T a \/ a T b ) ) )
85 83 84 bitr2i 
 |-  ( ( a = b \/ ( b T a \/ a T b ) ) <-> ( a T b \/ a = b \/ b T a ) )
86 82 85 sylib 
 |-  ( ( ph /\ ( a e. U /\ b e. U ) ) -> ( a T b \/ a = b \/ b T a ) )
87 11 86 issod 
 |-  ( ph -> T Or U )