Metamath Proof Explorer

Theorem relexp0eq

Description: The zeroth power of relationships is the same if and only if the union of their domain and ranges is the same. (Contributed by RP, 11-Jun-2020)

Ref Expression
Assertion relexp0eq 
|- ( ( A e. U /\ B e. V ) -> ( ( dom A u. ran A ) = ( dom B u. ran B ) <-> ( A ^r 0 ) = ( B ^r 0 ) ) )

Proof

Step Hyp Ref Expression
1 dfcleq 
 |-  ( ( dom A u. ran A ) = ( dom B u. ran B ) <-> A. x ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) )
2 alcom 
 |-  ( A. y A. x ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) <-> A. x A. y ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) )
3 19.3v 
 |-  ( A. y A. x ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) <-> A. x ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) )
4 ax6ev 
 |-  E. y y = x
5 pm5.5 
 |-  ( E. y y = x -> ( ( E. y y = x -> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) <-> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) )
6 4 5 ax-mp 
 |-  ( ( E. y y = x -> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) <-> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) )
7 19.23v 
 |-  ( A. y ( y = x -> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) <-> ( E. y y = x -> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) )
8 19.3v 
 |-  ( A. y ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) <-> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) )
9 6 7 8 3bitr4ri 
 |-  ( A. y ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) <-> A. y ( y = x -> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) )
10 pm5.32 
 |-  ( ( y = x -> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) <-> ( ( y = x /\ x e. ( dom A u. ran A ) ) <-> ( y = x /\ x e. ( dom B u. ran B ) ) ) )
11 ancom 
 |-  ( ( y = x /\ x e. ( dom A u. ran A ) ) <-> ( x e. ( dom A u. ran A ) /\ y = x ) )
12 ancom 
 |-  ( ( y = x /\ x e. ( dom B u. ran B ) ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) )
13 11 12 bibi12i 
 |-  ( ( ( y = x /\ x e. ( dom A u. ran A ) ) <-> ( y = x /\ x e. ( dom B u. ran B ) ) ) <-> ( ( x e. ( dom A u. ran A ) /\ y = x ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) ) )
14 10 13 bitri 
 |-  ( ( y = x -> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) <-> ( ( x e. ( dom A u. ran A ) /\ y = x ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) ) )
15 14 albii 
 |-  ( A. y ( y = x -> ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) ) <-> A. y ( ( x e. ( dom A u. ran A ) /\ y = x ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) ) )
16 9 15 bitri 
 |-  ( A. y ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) <-> A. y ( ( x e. ( dom A u. ran A ) /\ y = x ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) ) )
17 16 albii 
 |-  ( A. x A. y ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) <-> A. x A. y ( ( x e. ( dom A u. ran A ) /\ y = x ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) ) )
18 2 3 17 3bitr3i 
 |-  ( A. x ( x e. ( dom A u. ran A ) <-> x e. ( dom B u. ran B ) ) <-> A. x A. y ( ( x e. ( dom A u. ran A ) /\ y = x ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) ) )
19 1 18 bitri 
 |-  ( ( dom A u. ran A ) = ( dom B u. ran B ) <-> A. x A. y ( ( x e. ( dom A u. ran A ) /\ y = x ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) ) )
20 eqopab2bw 
 |-  ( { <. x , y >. | ( x e. ( dom A u. ran A ) /\ y = x ) } = { <. x , y >. | ( x e. ( dom B u. ran B ) /\ y = x ) } <-> A. x A. y ( ( x e. ( dom A u. ran A ) /\ y = x ) <-> ( x e. ( dom B u. ran B ) /\ y = x ) ) )
21 opabresid 
 |-  ( _I |` ( dom A u. ran A ) ) = { <. x , y >. | ( x e. ( dom A u. ran A ) /\ y = x ) }
22 21 eqcomi 
 |-  { <. x , y >. | ( x e. ( dom A u. ran A ) /\ y = x ) } = ( _I |` ( dom A u. ran A ) )
23 opabresid 
 |-  ( _I |` ( dom B u. ran B ) ) = { <. x , y >. | ( x e. ( dom B u. ran B ) /\ y = x ) }
24 23 eqcomi 
 |-  { <. x , y >. | ( x e. ( dom B u. ran B ) /\ y = x ) } = ( _I |` ( dom B u. ran B ) )
25 22 24 eqeq12i 
 |-  ( { <. x , y >. | ( x e. ( dom A u. ran A ) /\ y = x ) } = { <. x , y >. | ( x e. ( dom B u. ran B ) /\ y = x ) } <-> ( _I |` ( dom A u. ran A ) ) = ( _I |` ( dom B u. ran B ) ) )
26 19 20 25 3bitr2i 
 |-  ( ( dom A u. ran A ) = ( dom B u. ran B ) <-> ( _I |` ( dom A u. ran A ) ) = ( _I |` ( dom B u. ran B ) ) )
27 relexp0g 
 |-  ( A e. U -> ( A ^r 0 ) = ( _I |` ( dom A u. ran A ) ) )
28 relexp0g 
 |-  ( B e. V -> ( B ^r 0 ) = ( _I |` ( dom B u. ran B ) ) )
29 27 28 eqeqan12d 
 |-  ( ( A e. U /\ B e. V ) -> ( ( A ^r 0 ) = ( B ^r 0 ) <-> ( _I |` ( dom A u. ran A ) ) = ( _I |` ( dom B u. ran B ) ) ) )
30 26 29 bitr4id 
 |-  ( ( A e. U /\ B e. V ) -> ( ( dom A u. ran A ) = ( dom B u. ran B ) <-> ( A ^r 0 ) = ( B ^r 0 ) ) )