Metamath Proof Explorer

Theorem undmrnresiss

Description: Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg . (Contributed by RP, 26-Sep-2020)

Ref Expression
Assertion undmrnresiss 
|- ( ( _I |` ( dom A u. ran A ) ) C_ B <-> A. x A. y ( x A y -> ( x B x /\ y B y ) ) )

Proof

Step Hyp Ref Expression
1 resundi 
 |-  ( _I |` ( dom A u. ran A ) ) = ( ( _I |` dom A ) u. ( _I |` ran A ) )
2 1 sseq1i 
 |-  ( ( _I |` ( dom A u. ran A ) ) C_ B <-> ( ( _I |` dom A ) u. ( _I |` ran A ) ) C_ B )
3 unss 
 |-  ( ( ( _I |` dom A ) C_ B /\ ( _I |` ran A ) C_ B ) <-> ( ( _I |` dom A ) u. ( _I |` ran A ) ) C_ B )
4 relres 
 |-  Rel ( _I |` dom A )
5 ssrel 
 |-  ( Rel ( _I |` dom A ) -> ( ( _I |` dom A ) C_ B <-> A. x A. z ( <. x , z >. e. ( _I |` dom A ) -> <. x , z >. e. B ) ) )
6 4 5 ax-mp 
 |-  ( ( _I |` dom A ) C_ B <-> A. x A. z ( <. x , z >. e. ( _I |` dom A ) -> <. x , z >. e. B ) )
7 vex 
 |-  x e. _V
8 7 eldm 
 |-  ( x e. dom A <-> E. y x A y )
9 df-br 
 |-  ( x _I z <-> <. x , z >. e. _I )
10 vex 
 |-  z e. _V
11 10 ideq 
 |-  ( x _I z <-> x = z )
12 9 11 bitr3i 
 |-  ( <. x , z >. e. _I <-> x = z )
13 8 12 anbi12ci 
 |-  ( ( x e. dom A /\ <. x , z >. e. _I ) <-> ( x = z /\ E. y x A y ) )
14 10 opelresi 
 |-  ( <. x , z >. e. ( _I |` dom A ) <-> ( x e. dom A /\ <. x , z >. e. _I ) )
15 19.42v 
 |-  ( E. y ( x = z /\ x A y ) <-> ( x = z /\ E. y x A y ) )
16 13 14 15 3bitr4i 
 |-  ( <. x , z >. e. ( _I |` dom A ) <-> E. y ( x = z /\ x A y ) )
17 df-br 
 |-  ( x B z <-> <. x , z >. e. B )
18 17 bicomi 
 |-  ( <. x , z >. e. B <-> x B z )
19 16 18 imbi12i 
 |-  ( ( <. x , z >. e. ( _I |` dom A ) -> <. x , z >. e. B ) <-> ( E. y ( x = z /\ x A y ) -> x B z ) )
20 19 2albii 
 |-  ( A. x A. z ( <. x , z >. e. ( _I |` dom A ) -> <. x , z >. e. B ) <-> A. x A. z ( E. y ( x = z /\ x A y ) -> x B z ) )
21 19.23v 
 |-  ( A. y ( ( x = z /\ x A y ) -> x B z ) <-> ( E. y ( x = z /\ x A y ) -> x B z ) )
22 21 bicomi 
 |-  ( ( E. y ( x = z /\ x A y ) -> x B z ) <-> A. y ( ( x = z /\ x A y ) -> x B z ) )
23 22 2albii 
 |-  ( A. x A. z ( E. y ( x = z /\ x A y ) -> x B z ) <-> A. x A. z A. y ( ( x = z /\ x A y ) -> x B z ) )
24 alcom 
 |-  ( A. z A. y ( ( x = z /\ x A y ) -> x B z ) <-> A. y A. z ( ( x = z /\ x A y ) -> x B z ) )
25 ancomst 
 |-  ( ( ( x = z /\ x A y ) -> x B z ) <-> ( ( x A y /\ x = z ) -> x B z ) )
26 impexp 
 |-  ( ( ( x A y /\ x = z ) -> x B z ) <-> ( x A y -> ( x = z -> x B z ) ) )
27 25 26 bitri 
 |-  ( ( ( x = z /\ x A y ) -> x B z ) <-> ( x A y -> ( x = z -> x B z ) ) )
28 27 albii 
 |-  ( A. z ( ( x = z /\ x A y ) -> x B z ) <-> A. z ( x A y -> ( x = z -> x B z ) ) )
29 19.21v 
 |-  ( A. z ( x A y -> ( x = z -> x B z ) ) <-> ( x A y -> A. z ( x = z -> x B z ) ) )
30 equcom 
 |-  ( x = z <-> z = x )
31 30 imbi1i 
 |-  ( ( x = z -> x B z ) <-> ( z = x -> x B z ) )
32 31 albii 
 |-  ( A. z ( x = z -> x B z ) <-> A. z ( z = x -> x B z ) )
33 breq2 
 |-  ( z = x -> ( x B z <-> x B x ) )
34 33 equsalvw 
 |-  ( A. z ( z = x -> x B z ) <-> x B x )
35 32 34 bitri 
 |-  ( A. z ( x = z -> x B z ) <-> x B x )
36 35 imbi2i 
 |-  ( ( x A y -> A. z ( x = z -> x B z ) ) <-> ( x A y -> x B x ) )
37 28 29 36 3bitri 
 |-  ( A. z ( ( x = z /\ x A y ) -> x B z ) <-> ( x A y -> x B x ) )
38 37 albii 
 |-  ( A. y A. z ( ( x = z /\ x A y ) -> x B z ) <-> A. y ( x A y -> x B x ) )
39 24 38 bitri 
 |-  ( A. z A. y ( ( x = z /\ x A y ) -> x B z ) <-> A. y ( x A y -> x B x ) )
40 39 albii 
 |-  ( A. x A. z A. y ( ( x = z /\ x A y ) -> x B z ) <-> A. x A. y ( x A y -> x B x ) )
41 23 40 bitri 
 |-  ( A. x A. z ( E. y ( x = z /\ x A y ) -> x B z ) <-> A. x A. y ( x A y -> x B x ) )
42 6 20 41 3bitri 
 |-  ( ( _I |` dom A ) C_ B <-> A. x A. y ( x A y -> x B x ) )
43 relres 
 |-  Rel ( _I |` ran A )
44 ssrel 
 |-  ( Rel ( _I |` ran A ) -> ( ( _I |` ran A ) C_ B <-> A. y A. z ( <. y , z >. e. ( _I |` ran A ) -> <. y , z >. e. B ) ) )
45 43 44 ax-mp 
 |-  ( ( _I |` ran A ) C_ B <-> A. y A. z ( <. y , z >. e. ( _I |` ran A ) -> <. y , z >. e. B ) )
46 vex 
 |-  y e. _V
47 46 elrn 
 |-  ( y e. ran A <-> E. x x A y )
48 df-br 
 |-  ( y _I z <-> <. y , z >. e. _I )
49 10 ideq 
 |-  ( y _I z <-> y = z )
50 48 49 bitr3i 
 |-  ( <. y , z >. e. _I <-> y = z )
51 47 50 anbi12ci 
 |-  ( ( y e. ran A /\ <. y , z >. e. _I ) <-> ( y = z /\ E. x x A y ) )
52 10 opelresi 
 |-  ( <. y , z >. e. ( _I |` ran A ) <-> ( y e. ran A /\ <. y , z >. e. _I ) )
53 19.42v 
 |-  ( E. x ( y = z /\ x A y ) <-> ( y = z /\ E. x x A y ) )
54 51 52 53 3bitr4i 
 |-  ( <. y , z >. e. ( _I |` ran A ) <-> E. x ( y = z /\ x A y ) )
55 df-br 
 |-  ( y B z <-> <. y , z >. e. B )
56 55 bicomi 
 |-  ( <. y , z >. e. B <-> y B z )
57 54 56 imbi12i 
 |-  ( ( <. y , z >. e. ( _I |` ran A ) -> <. y , z >. e. B ) <-> ( E. x ( y = z /\ x A y ) -> y B z ) )
58 57 2albii 
 |-  ( A. y A. z ( <. y , z >. e. ( _I |` ran A ) -> <. y , z >. e. B ) <-> A. y A. z ( E. x ( y = z /\ x A y ) -> y B z ) )
59 19.23v 
 |-  ( A. x ( ( y = z /\ x A y ) -> y B z ) <-> ( E. x ( y = z /\ x A y ) -> y B z ) )
60 59 bicomi 
 |-  ( ( E. x ( y = z /\ x A y ) -> y B z ) <-> A. x ( ( y = z /\ x A y ) -> y B z ) )
61 60 2albii 
 |-  ( A. y A. z ( E. x ( y = z /\ x A y ) -> y B z ) <-> A. y A. z A. x ( ( y = z /\ x A y ) -> y B z ) )
62 alrot3 
 |-  ( A. x A. y A. z ( ( y = z /\ x A y ) -> y B z ) <-> A. y A. z A. x ( ( y = z /\ x A y ) -> y B z ) )
63 ancomst 
 |-  ( ( ( y = z /\ x A y ) -> y B z ) <-> ( ( x A y /\ y = z ) -> y B z ) )
64 impexp 
 |-  ( ( ( x A y /\ y = z ) -> y B z ) <-> ( x A y -> ( y = z -> y B z ) ) )
65 63 64 bitri 
 |-  ( ( ( y = z /\ x A y ) -> y B z ) <-> ( x A y -> ( y = z -> y B z ) ) )
66 65 albii 
 |-  ( A. z ( ( y = z /\ x A y ) -> y B z ) <-> A. z ( x A y -> ( y = z -> y B z ) ) )
67 19.21v 
 |-  ( A. z ( x A y -> ( y = z -> y B z ) ) <-> ( x A y -> A. z ( y = z -> y B z ) ) )
68 equcom 
 |-  ( y = z <-> z = y )
69 68 imbi1i 
 |-  ( ( y = z -> y B z ) <-> ( z = y -> y B z ) )
70 69 albii 
 |-  ( A. z ( y = z -> y B z ) <-> A. z ( z = y -> y B z ) )
71 breq2 
 |-  ( z = y -> ( y B z <-> y B y ) )
72 71 equsalvw 
 |-  ( A. z ( z = y -> y B z ) <-> y B y )
73 70 72 bitri 
 |-  ( A. z ( y = z -> y B z ) <-> y B y )
74 73 imbi2i 
 |-  ( ( x A y -> A. z ( y = z -> y B z ) ) <-> ( x A y -> y B y ) )
75 66 67 74 3bitri 
 |-  ( A. z ( ( y = z /\ x A y ) -> y B z ) <-> ( x A y -> y B y ) )
76 75 2albii 
 |-  ( A. x A. y A. z ( ( y = z /\ x A y ) -> y B z ) <-> A. x A. y ( x A y -> y B y ) )
77 61 62 76 3bitr2i 
 |-  ( A. y A. z ( E. x ( y = z /\ x A y ) -> y B z ) <-> A. x A. y ( x A y -> y B y ) )
78 45 58 77 3bitri 
 |-  ( ( _I |` ran A ) C_ B <-> A. x A. y ( x A y -> y B y ) )
79 42 78 anbi12i 
 |-  ( ( ( _I |` dom A ) C_ B /\ ( _I |` ran A ) C_ B ) <-> ( A. x A. y ( x A y -> x B x ) /\ A. x A. y ( x A y -> y B y ) ) )
80 19.26-2 
 |-  ( A. x A. y ( ( x A y -> x B x ) /\ ( x A y -> y B y ) ) <-> ( A. x A. y ( x A y -> x B x ) /\ A. x A. y ( x A y -> y B y ) ) )
81 pm4.76 
 |-  ( ( ( x A y -> x B x ) /\ ( x A y -> y B y ) ) <-> ( x A y -> ( x B x /\ y B y ) ) )
82 81 2albii 
 |-  ( A. x A. y ( ( x A y -> x B x ) /\ ( x A y -> y B y ) ) <-> A. x A. y ( x A y -> ( x B x /\ y B y ) ) )
83 79 80 82 3bitr2i 
 |-  ( ( ( _I |` dom A ) C_ B /\ ( _I |` ran A ) C_ B ) <-> A. x A. y ( x A y -> ( x B x /\ y B y ) ) )
84 2 3 83 3bitr2i 
 |-  ( ( _I |` ( dom A u. ran A ) ) C_ B <-> A. x A. y ( x A y -> ( x B x /\ y B y ) ) )