Metamath Proof Explorer

Theorem relexp0a

Description: Absorbtion law for zeroth power of a relation. (Contributed by RP, 17-Jun-2020)

Ref Expression
Assertion relexp0a 
|- ( ( A e. V /\ N e. NN0 ) -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 oveq2 
 |-  ( x = 1 -> ( A ^r x ) = ( A ^r 1 ) )
3 2 oveq1d 
 |-  ( x = 1 -> ( ( A ^r x ) ^r 0 ) = ( ( A ^r 1 ) ^r 0 ) )
4 3 sseq1d 
 |-  ( x = 1 -> ( ( ( A ^r x ) ^r 0 ) C_ ( A ^r 0 ) <-> ( ( A ^r 1 ) ^r 0 ) C_ ( A ^r 0 ) ) )
5 4 imbi2d 
 |-  ( x = 1 -> ( ( A e. V -> ( ( A ^r x ) ^r 0 ) C_ ( A ^r 0 ) ) <-> ( A e. V -> ( ( A ^r 1 ) ^r 0 ) C_ ( A ^r 0 ) ) ) )
6 oveq2 
 |-  ( x = y -> ( A ^r x ) = ( A ^r y ) )
7 6 oveq1d 
 |-  ( x = y -> ( ( A ^r x ) ^r 0 ) = ( ( A ^r y ) ^r 0 ) )
8 7 sseq1d 
 |-  ( x = y -> ( ( ( A ^r x ) ^r 0 ) C_ ( A ^r 0 ) <-> ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) )
9 8 imbi2d 
 |-  ( x = y -> ( ( A e. V -> ( ( A ^r x ) ^r 0 ) C_ ( A ^r 0 ) ) <-> ( A e. V -> ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) ) )
10 oveq2 
 |-  ( x = ( y + 1 ) -> ( A ^r x ) = ( A ^r ( y + 1 ) ) )
11 10 oveq1d 
 |-  ( x = ( y + 1 ) -> ( ( A ^r x ) ^r 0 ) = ( ( A ^r ( y + 1 ) ) ^r 0 ) )
12 11 sseq1d 
 |-  ( x = ( y + 1 ) -> ( ( ( A ^r x ) ^r 0 ) C_ ( A ^r 0 ) <-> ( ( A ^r ( y + 1 ) ) ^r 0 ) C_ ( A ^r 0 ) ) )
13 12 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( A e. V -> ( ( A ^r x ) ^r 0 ) C_ ( A ^r 0 ) ) <-> ( A e. V -> ( ( A ^r ( y + 1 ) ) ^r 0 ) C_ ( A ^r 0 ) ) ) )
14 oveq2 
 |-  ( x = N -> ( A ^r x ) = ( A ^r N ) )
15 14 oveq1d 
 |-  ( x = N -> ( ( A ^r x ) ^r 0 ) = ( ( A ^r N ) ^r 0 ) )
16 15 sseq1d 
 |-  ( x = N -> ( ( ( A ^r x ) ^r 0 ) C_ ( A ^r 0 ) <-> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) ) )
17 16 imbi2d 
 |-  ( x = N -> ( ( A e. V -> ( ( A ^r x ) ^r 0 ) C_ ( A ^r 0 ) ) <-> ( A e. V -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) ) ) )
18 relexp1g 
 |-  ( A e. V -> ( A ^r 1 ) = A )
19 18 oveq1d 
 |-  ( A e. V -> ( ( A ^r 1 ) ^r 0 ) = ( A ^r 0 ) )
20 ssid 
 |-  ( A ^r 0 ) C_ ( A ^r 0 )
21 19 20 eqsstrdi 
 |-  ( A e. V -> ( ( A ^r 1 ) ^r 0 ) C_ ( A ^r 0 ) )
22 simp2 
 |-  ( ( y e. NN /\ A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> A e. V )
23 simp1 
 |-  ( ( y e. NN /\ A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> y e. NN )
24 relexpsucnnr 
 |-  ( ( A e. V /\ y e. NN ) -> ( A ^r ( y + 1 ) ) = ( ( A ^r y ) o. A ) )
25 24 oveq1d 
 |-  ( ( A e. V /\ y e. NN ) -> ( ( A ^r ( y + 1 ) ) ^r 0 ) = ( ( ( A ^r y ) o. A ) ^r 0 ) )
26 22 23 25 syl2anc 
 |-  ( ( y e. NN /\ A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( ( A ^r ( y + 1 ) ) ^r 0 ) = ( ( ( A ^r y ) o. A ) ^r 0 ) )
27 ovex 
 |-  ( A ^r y ) e. _V
28 coexg 
 |-  ( ( ( A ^r y ) e. _V /\ A e. V ) -> ( ( A ^r y ) o. A ) e. _V )
29 27 28 mpan 
 |-  ( A e. V -> ( ( A ^r y ) o. A ) e. _V )
30 relexp0g 
 |-  ( ( ( A ^r y ) o. A ) e. _V -> ( ( ( A ^r y ) o. A ) ^r 0 ) = ( _I |` ( dom ( ( A ^r y ) o. A ) u. ran ( ( A ^r y ) o. A ) ) ) )
31 29 30 syl 
 |-  ( A e. V -> ( ( ( A ^r y ) o. A ) ^r 0 ) = ( _I |` ( dom ( ( A ^r y ) o. A ) u. ran ( ( A ^r y ) o. A ) ) ) )
32 dmcoss 
 |-  dom ( ( A ^r y ) o. A ) C_ dom A
33 rncoss 
 |-  ran ( ( A ^r y ) o. A ) C_ ran ( A ^r y )
34 unss12 
 |-  ( ( dom ( ( A ^r y ) o. A ) C_ dom A /\ ran ( ( A ^r y ) o. A ) C_ ran ( A ^r y ) ) -> ( dom ( ( A ^r y ) o. A ) u. ran ( ( A ^r y ) o. A ) ) C_ ( dom A u. ran ( A ^r y ) ) )
35 32 33 34 mp2an 
 |-  ( dom ( ( A ^r y ) o. A ) u. ran ( ( A ^r y ) o. A ) ) C_ ( dom A u. ran ( A ^r y ) )
36 ssres2 
 |-  ( ( dom ( ( A ^r y ) o. A ) u. ran ( ( A ^r y ) o. A ) ) C_ ( dom A u. ran ( A ^r y ) ) -> ( _I |` ( dom ( ( A ^r y ) o. A ) u. ran ( ( A ^r y ) o. A ) ) ) C_ ( _I |` ( dom A u. ran ( A ^r y ) ) ) )
37 35 36 ax-mp 
 |-  ( _I |` ( dom ( ( A ^r y ) o. A ) u. ran ( ( A ^r y ) o. A ) ) ) C_ ( _I |` ( dom A u. ran ( A ^r y ) ) )
38 31 37 eqsstrdi 
 |-  ( A e. V -> ( ( ( A ^r y ) o. A ) ^r 0 ) C_ ( _I |` ( dom A u. ran ( A ^r y ) ) ) )
39 22 38 syl 
 |-  ( ( y e. NN /\ A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( ( ( A ^r y ) o. A ) ^r 0 ) C_ ( _I |` ( dom A u. ran ( A ^r y ) ) ) )
40 resundi 
 |-  ( _I |` ( dom A u. ran ( A ^r y ) ) ) = ( ( _I |` dom A ) u. ( _I |` ran ( A ^r y ) ) )
41 ssun1 
 |-  dom A C_ ( dom A u. ran A )
42 ssres2 
 |-  ( dom A C_ ( dom A u. ran A ) -> ( _I |` dom A ) C_ ( _I |` ( dom A u. ran A ) ) )
43 41 42 ax-mp 
 |-  ( _I |` dom A ) C_ ( _I |` ( dom A u. ran A ) )
44 relexp0g 
 |-  ( A e. V -> ( A ^r 0 ) = ( _I |` ( dom A u. ran A ) ) )
45 43 44 sseqtrrid 
 |-  ( A e. V -> ( _I |` dom A ) C_ ( A ^r 0 ) )
46 45 adantr 
 |-  ( ( A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( _I |` dom A ) C_ ( A ^r 0 ) )
47 ssun2 
 |-  ran ( A ^r y ) C_ ( dom ( A ^r y ) u. ran ( A ^r y ) )
48 ssres2 
 |-  ( ran ( A ^r y ) C_ ( dom ( A ^r y ) u. ran ( A ^r y ) ) -> ( _I |` ran ( A ^r y ) ) C_ ( _I |` ( dom ( A ^r y ) u. ran ( A ^r y ) ) ) )
49 47 48 ax-mp 
 |-  ( _I |` ran ( A ^r y ) ) C_ ( _I |` ( dom ( A ^r y ) u. ran ( A ^r y ) ) )
50 relexp0g 
 |-  ( ( A ^r y ) e. _V -> ( ( A ^r y ) ^r 0 ) = ( _I |` ( dom ( A ^r y ) u. ran ( A ^r y ) ) ) )
51 27 50 ax-mp 
 |-  ( ( A ^r y ) ^r 0 ) = ( _I |` ( dom ( A ^r y ) u. ran ( A ^r y ) ) )
52 49 51 sseqtrri 
 |-  ( _I |` ran ( A ^r y ) ) C_ ( ( A ^r y ) ^r 0 )
53 simpr 
 |-  ( ( A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) )
54 52 53 sstrid 
 |-  ( ( A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( _I |` ran ( A ^r y ) ) C_ ( A ^r 0 ) )
55 46 54 unssd 
 |-  ( ( A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( ( _I |` dom A ) u. ( _I |` ran ( A ^r y ) ) ) C_ ( A ^r 0 ) )
56 40 55 eqsstrid 
 |-  ( ( A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( _I |` ( dom A u. ran ( A ^r y ) ) ) C_ ( A ^r 0 ) )
57 56 3adant1 
 |-  ( ( y e. NN /\ A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( _I |` ( dom A u. ran ( A ^r y ) ) ) C_ ( A ^r 0 ) )
58 39 57 sstrd 
 |-  ( ( y e. NN /\ A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( ( ( A ^r y ) o. A ) ^r 0 ) C_ ( A ^r 0 ) )
59 26 58 eqsstrd 
 |-  ( ( y e. NN /\ A e. V /\ ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( ( A ^r ( y + 1 ) ) ^r 0 ) C_ ( A ^r 0 ) )
60 59 3exp 
 |-  ( y e. NN -> ( A e. V -> ( ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) -> ( ( A ^r ( y + 1 ) ) ^r 0 ) C_ ( A ^r 0 ) ) ) )
61 60 a2d 
 |-  ( y e. NN -> ( ( A e. V -> ( ( A ^r y ) ^r 0 ) C_ ( A ^r 0 ) ) -> ( A e. V -> ( ( A ^r ( y + 1 ) ) ^r 0 ) C_ ( A ^r 0 ) ) ) )
62 5 9 13 17 21 61 nnind 
 |-  ( N e. NN -> ( A e. V -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) ) )
63 oveq2 
 |-  ( N = 0 -> ( A ^r N ) = ( A ^r 0 ) )
64 63 oveq1d 
 |-  ( N = 0 -> ( ( A ^r N ) ^r 0 ) = ( ( A ^r 0 ) ^r 0 ) )
65 relexp0idm 
 |-  ( A e. V -> ( ( A ^r 0 ) ^r 0 ) = ( A ^r 0 ) )
66 64 65 sylan9eq 
 |-  ( ( N = 0 /\ A e. V ) -> ( ( A ^r N ) ^r 0 ) = ( A ^r 0 ) )
67 eqimss 
 |-  ( ( ( A ^r N ) ^r 0 ) = ( A ^r 0 ) -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) )
68 66 67 syl 
 |-  ( ( N = 0 /\ A e. V ) -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) )
69 68 ex 
 |-  ( N = 0 -> ( A e. V -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) ) )
70 62 69 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( A e. V -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) ) )
71 1 70 sylbi 
 |-  ( N e. NN0 -> ( A e. V -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) ) )
72 71 impcom 
 |-  ( ( A e. V /\ N e. NN0 ) -> ( ( A ^r N ) ^r 0 ) C_ ( A ^r 0 ) )