Metamath Proof Explorer

Theorem iunrelexp0

Description: Simplification of zeroth power of indexed union of powers of relations. (Contributed by RP, 19-Jun-2020)

Ref Expression
Assertion iunrelexp0 
|- ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( U_ x e. Z ( R ^r x ) ^r 0 ) = ( R ^r 0 ) )

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { 0 , 1 } = ( { 0 } u. { 1 } )
2 1 ineq1i 
 |-  ( { 0 , 1 } i^i Z ) = ( ( { 0 } u. { 1 } ) i^i Z )
3 indir 
 |-  ( ( { 0 } u. { 1 } ) i^i Z ) = ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) )
4 2 3 eqtr2i 
 |-  ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) = ( { 0 , 1 } i^i Z )
5 4 uneq1i 
 |-  ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) = ( ( { 0 , 1 } i^i Z ) u. Z )
6 inss2 
 |-  ( { 0 , 1 } i^i Z ) C_ Z
7 ssequn1 
 |-  ( ( { 0 , 1 } i^i Z ) C_ Z <-> ( ( { 0 , 1 } i^i Z ) u. Z ) = Z )
8 6 7 mpbi 
 |-  ( ( { 0 , 1 } i^i Z ) u. Z ) = Z
9 5 8 eqtr2i 
 |-  Z = ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z )
10 iuneq1 
 |-  ( Z = ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) -> U_ x e. Z ( R ^r x ) = U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) )
11 10 oveq1d 
 |-  ( Z = ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) -> ( U_ x e. Z ( R ^r x ) ^r 0 ) = ( U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ^r 0 ) )
12 9 11 ax-mp 
 |-  ( U_ x e. Z ( R ^r x ) ^r 0 ) = ( U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ^r 0 )
13 dmiun 
 |-  dom U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) = U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) dom ( R ^r x )
14 iunxun 
 |-  U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) dom ( R ^r x ) = ( U_ x e. ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) dom ( R ^r x ) u. U_ x e. Z dom ( R ^r x ) )
15 iunxun 
 |-  U_ x e. ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) dom ( R ^r x ) = ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) )
16 15 equncomi 
 |-  U_ x e. ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) dom ( R ^r x ) = ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) )
17 16 uneq1i 
 |-  ( U_ x e. ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) dom ( R ^r x ) u. U_ x e. Z dom ( R ^r x ) ) = ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. U_ x e. Z dom ( R ^r x ) )
18 17 equncomi 
 |-  ( U_ x e. ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) dom ( R ^r x ) u. U_ x e. Z dom ( R ^r x ) ) = ( U_ x e. Z dom ( R ^r x ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) )
19 13 14 18 3eqtri 
 |-  dom U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) = ( U_ x e. Z dom ( R ^r x ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) )
20 rniun 
 |-  ran U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) = U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ran ( R ^r x )
21 iunxun 
 |-  U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ran ( R ^r x ) = ( U_ x e. ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) ran ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) )
22 iunxun 
 |-  U_ x e. ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) ran ( R ^r x ) = ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) )
23 22 uneq1i 
 |-  ( U_ x e. ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) ran ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) = ( ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) u. U_ x e. Z ran ( R ^r x ) )
24 20 21 23 3eqtri 
 |-  ran U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) = ( ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) u. U_ x e. Z ran ( R ^r x ) )
25 19 24 uneq12i 
 |-  ( dom U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) u. ran U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ) = ( ( U_ x e. Z dom ( R ^r x ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) ) u. ( ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) u. U_ x e. Z ran ( R ^r x ) ) )
26 uncom 
 |-  ( U_ x e. Z dom ( R ^r x ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) ) = ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. U_ x e. Z dom ( R ^r x ) )
27 26 uneq1i 
 |-  ( ( U_ x e. Z dom ( R ^r x ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) ) u. ( ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) u. U_ x e. Z ran ( R ^r x ) ) ) = ( ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. U_ x e. Z dom ( R ^r x ) ) u. ( ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) u. U_ x e. Z ran ( R ^r x ) ) )
28 un4 
 |-  ( ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. U_ x e. Z dom ( R ^r x ) ) u. ( ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) u. U_ x e. Z ran ( R ^r x ) ) ) = ( ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) )
29 27 28 eqtri 
 |-  ( ( U_ x e. Z dom ( R ^r x ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) ) u. ( ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) u. U_ x e. Z ran ( R ^r x ) ) ) = ( ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) )
30 uncom 
 |-  ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) = ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) )
31 30 uneq1i 
 |-  ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) ) u. ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) )
32 un4 
 |-  ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) ) u. ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) )
33 31 32 eqtri 
 |-  ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) )
34 33 uneq1i 
 |-  ( ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) ) u. ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) ) = ( ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) )
35 25 29 34 3eqtri 
 |-  ( dom U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) u. ran U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ) = ( ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) )
36 df-ne 
 |-  ( ( { 0 , 1 } i^i Z ) =/= (/) <-> -. ( { 0 , 1 } i^i Z ) = (/) )
37 incom 
 |-  ( { 0 , 1 } i^i Z ) = ( Z i^i { 0 , 1 } )
38 1 ineq2i 
 |-  ( Z i^i { 0 , 1 } ) = ( Z i^i ( { 0 } u. { 1 } ) )
39 indi 
 |-  ( Z i^i ( { 0 } u. { 1 } ) ) = ( ( Z i^i { 0 } ) u. ( Z i^i { 1 } ) )
40 37 38 39 3eqtri 
 |-  ( { 0 , 1 } i^i Z ) = ( ( Z i^i { 0 } ) u. ( Z i^i { 1 } ) )
41 40 eqeq1i 
 |-  ( ( { 0 , 1 } i^i Z ) = (/) <-> ( ( Z i^i { 0 } ) u. ( Z i^i { 1 } ) ) = (/) )
42 un00 
 |-  ( ( ( Z i^i { 0 } ) = (/) /\ ( Z i^i { 1 } ) = (/) ) <-> ( ( Z i^i { 0 } ) u. ( Z i^i { 1 } ) ) = (/) )
43 anor 
 |-  ( ( ( Z i^i { 0 } ) = (/) /\ ( Z i^i { 1 } ) = (/) ) <-> -. ( -. ( Z i^i { 0 } ) = (/) \/ -. ( Z i^i { 1 } ) = (/) ) )
44 41 42 43 3bitr2i 
 |-  ( ( { 0 , 1 } i^i Z ) = (/) <-> -. ( -. ( Z i^i { 0 } ) = (/) \/ -. ( Z i^i { 1 } ) = (/) ) )
45 44 notbii 
 |-  ( -. ( { 0 , 1 } i^i Z ) = (/) <-> -. -. ( -. ( Z i^i { 0 } ) = (/) \/ -. ( Z i^i { 1 } ) = (/) ) )
46 notnotb 
 |-  ( ( -. ( Z i^i { 0 } ) = (/) \/ -. ( Z i^i { 1 } ) = (/) ) <-> -. -. ( -. ( Z i^i { 0 } ) = (/) \/ -. ( Z i^i { 1 } ) = (/) ) )
47 disjsn 
 |-  ( ( Z i^i { 0 } ) = (/) <-> -. 0 e. Z )
48 47 notbii 
 |-  ( -. ( Z i^i { 0 } ) = (/) <-> -. -. 0 e. Z )
49 notnotb 
 |-  ( 0 e. Z <-> -. -. 0 e. Z )
50 48 49 bitr4i 
 |-  ( -. ( Z i^i { 0 } ) = (/) <-> 0 e. Z )
51 disjsn 
 |-  ( ( Z i^i { 1 } ) = (/) <-> -. 1 e. Z )
52 51 notbii 
 |-  ( -. ( Z i^i { 1 } ) = (/) <-> -. -. 1 e. Z )
53 notnotb 
 |-  ( 1 e. Z <-> -. -. 1 e. Z )
54 52 53 bitr4i 
 |-  ( -. ( Z i^i { 1 } ) = (/) <-> 1 e. Z )
55 50 54 orbi12i 
 |-  ( ( -. ( Z i^i { 0 } ) = (/) \/ -. ( Z i^i { 1 } ) = (/) ) <-> ( 0 e. Z \/ 1 e. Z ) )
56 45 46 55 3bitr2i 
 |-  ( -. ( { 0 , 1 } i^i Z ) = (/) <-> ( 0 e. Z \/ 1 e. Z ) )
57 36 56 sylbb 
 |-  ( ( { 0 , 1 } i^i Z ) =/= (/) -> ( 0 e. Z \/ 1 e. Z ) )
58 simpl 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> 0 e. Z )
59 58 snssd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> { 0 } C_ Z )
60 df-ss 
 |-  ( { 0 } C_ Z <-> ( { 0 } i^i Z ) = { 0 } )
61 59 60 sylib 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( { 0 } i^i Z ) = { 0 } )
62 61 iuneq1d 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) = U_ x e. { 0 } dom ( R ^r x ) )
63 c0ex 
 |-  0 e. _V
64 oveq2 
 |-  ( x = 0 -> ( R ^r x ) = ( R ^r 0 ) )
65 64 dmeqd 
 |-  ( x = 0 -> dom ( R ^r x ) = dom ( R ^r 0 ) )
66 63 65 iunxsn 
 |-  U_ x e. { 0 } dom ( R ^r x ) = dom ( R ^r 0 )
67 62 66 eqtrdi 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) = dom ( R ^r 0 ) )
68 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
69 68 ad2antll 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
70 69 dmeqd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> dom ( R ^r 0 ) = dom ( _I |` ( dom R u. ran R ) ) )
71 dmresi 
 |-  dom ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
72 70 71 eqtrdi 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> dom ( R ^r 0 ) = ( dom R u. ran R ) )
73 67 72 eqtrd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) = ( dom R u. ran R ) )
74 61 iuneq1d 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) = U_ x e. { 0 } ran ( R ^r x ) )
75 64 rneqd 
 |-  ( x = 0 -> ran ( R ^r x ) = ran ( R ^r 0 ) )
76 63 75 iunxsn 
 |-  U_ x e. { 0 } ran ( R ^r x ) = ran ( R ^r 0 )
77 74 76 eqtrdi 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) = ran ( R ^r 0 ) )
78 69 rneqd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ran ( R ^r 0 ) = ran ( _I |` ( dom R u. ran R ) ) )
79 rnresi 
 |-  ran ( _I |` ( dom R u. ran R ) ) = ( dom R u. ran R )
80 78 79 eqtrdi 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ran ( R ^r 0 ) = ( dom R u. ran R ) )
81 77 80 eqtrd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) = ( dom R u. ran R ) )
82 73 81 uneq12d 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) = ( ( dom R u. ran R ) u. ( dom R u. ran R ) ) )
83 unidm 
 |-  ( ( dom R u. ran R ) u. ( dom R u. ran R ) ) = ( dom R u. ran R )
84 82 83 eqtrdi 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) = ( dom R u. ran R ) )
85 84 uneq1d 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( ( dom R u. ran R ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) )
86 relexpdmg 
 |-  ( ( x e. NN0 /\ R e. V ) -> dom ( R ^r x ) C_ ( dom R u. ran R ) )
87 86 expcom 
 |-  ( R e. V -> ( x e. NN0 -> dom ( R ^r x ) C_ ( dom R u. ran R ) ) )
88 87 ralrimiv 
 |-  ( R e. V -> A. x e. NN0 dom ( R ^r x ) C_ ( dom R u. ran R ) )
89 88 ad2antll 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> A. x e. NN0 dom ( R ^r x ) C_ ( dom R u. ran R ) )
90 olc 
 |-  ( Z C_ NN0 -> ( { 1 } C_ NN0 \/ Z C_ NN0 ) )
91 90 ad2antrl 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( { 1 } C_ NN0 \/ Z C_ NN0 ) )
92 inss 
 |-  ( ( { 1 } C_ NN0 \/ Z C_ NN0 ) -> ( { 1 } i^i Z ) C_ NN0 )
93 91 92 syl 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( { 1 } i^i Z ) C_ NN0 )
94 93 sseld 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( x e. ( { 1 } i^i Z ) -> x e. NN0 ) )
95 94 imim1d 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( x e. NN0 -> dom ( R ^r x ) C_ ( dom R u. ran R ) ) -> ( x e. ( { 1 } i^i Z ) -> dom ( R ^r x ) C_ ( dom R u. ran R ) ) ) )
96 95 ralimdv2 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( A. x e. NN0 dom ( R ^r x ) C_ ( dom R u. ran R ) -> A. x e. ( { 1 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) ) )
97 89 96 mpd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> A. x e. ( { 1 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) )
98 iunss 
 |-  ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) <-> A. x e. ( { 1 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) )
99 97 98 sylibr 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) )
100 relexprng 
 |-  ( ( x e. NN0 /\ R e. V ) -> ran ( R ^r x ) C_ ( dom R u. ran R ) )
101 100 expcom 
 |-  ( R e. V -> ( x e. NN0 -> ran ( R ^r x ) C_ ( dom R u. ran R ) ) )
102 101 ralrimiv 
 |-  ( R e. V -> A. x e. NN0 ran ( R ^r x ) C_ ( dom R u. ran R ) )
103 102 ad2antll 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> A. x e. NN0 ran ( R ^r x ) C_ ( dom R u. ran R ) )
104 94 imim1d 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( x e. NN0 -> ran ( R ^r x ) C_ ( dom R u. ran R ) ) -> ( x e. ( { 1 } i^i Z ) -> ran ( R ^r x ) C_ ( dom R u. ran R ) ) ) )
105 104 ralimdv2 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( A. x e. NN0 ran ( R ^r x ) C_ ( dom R u. ran R ) -> A. x e. ( { 1 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) ) )
106 103 105 mpd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> A. x e. ( { 1 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) )
107 iunss 
 |-  ( U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) <-> A. x e. ( { 1 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) )
108 106 107 sylibr 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) )
109 99 108 unssd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) C_ ( dom R u. ran R ) )
110 ssequn2 
 |-  ( ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) C_ ( dom R u. ran R ) <-> ( ( dom R u. ran R ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
111 109 110 sylib 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( dom R u. ran R ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
112 85 111 eqtrd 
 |-  ( ( 0 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
113 112 ex 
 |-  ( 0 e. Z -> ( ( Z C_ NN0 /\ R e. V ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) ) )
114 simpl 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> 1 e. Z )
115 114 snssd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> { 1 } C_ Z )
116 df-ss 
 |-  ( { 1 } C_ Z <-> ( { 1 } i^i Z ) = { 1 } )
117 115 116 sylib 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( { 1 } i^i Z ) = { 1 } )
118 117 iuneq1d 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) = U_ x e. { 1 } dom ( R ^r x ) )
119 1ex 
 |-  1 e. _V
120 oveq2 
 |-  ( x = 1 -> ( R ^r x ) = ( R ^r 1 ) )
121 120 dmeqd 
 |-  ( x = 1 -> dom ( R ^r x ) = dom ( R ^r 1 ) )
122 119 121 iunxsn 
 |-  U_ x e. { 1 } dom ( R ^r x ) = dom ( R ^r 1 )
123 118 122 eqtrdi 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) = dom ( R ^r 1 ) )
124 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
125 124 ad2antll 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( R ^r 1 ) = R )
126 125 dmeqd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> dom ( R ^r 1 ) = dom R )
127 123 126 eqtrd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) = dom R )
128 117 iuneq1d 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) = U_ x e. { 1 } ran ( R ^r x ) )
129 120 rneqd 
 |-  ( x = 1 -> ran ( R ^r x ) = ran ( R ^r 1 ) )
130 119 129 iunxsn 
 |-  U_ x e. { 1 } ran ( R ^r x ) = ran ( R ^r 1 )
131 128 130 eqtrdi 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) = ran ( R ^r 1 ) )
132 125 rneqd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ran ( R ^r 1 ) = ran R )
133 131 132 eqtrd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) = ran R )
134 127 133 uneq12d 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) = ( dom R u. ran R ) )
135 134 uneq2d 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( dom R u. ran R ) ) )
136 88 ad2antll 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> A. x e. NN0 dom ( R ^r x ) C_ ( dom R u. ran R ) )
137 olc 
 |-  ( Z C_ NN0 -> ( { 0 } C_ NN0 \/ Z C_ NN0 ) )
138 137 ad2antrl 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( { 0 } C_ NN0 \/ Z C_ NN0 ) )
139 inss 
 |-  ( ( { 0 } C_ NN0 \/ Z C_ NN0 ) -> ( { 0 } i^i Z ) C_ NN0 )
140 138 139 syl 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( { 0 } i^i Z ) C_ NN0 )
141 140 sseld 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( x e. ( { 0 } i^i Z ) -> x e. NN0 ) )
142 141 imim1d 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( x e. NN0 -> dom ( R ^r x ) C_ ( dom R u. ran R ) ) -> ( x e. ( { 0 } i^i Z ) -> dom ( R ^r x ) C_ ( dom R u. ran R ) ) ) )
143 142 ralimdv2 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( A. x e. NN0 dom ( R ^r x ) C_ ( dom R u. ran R ) -> A. x e. ( { 0 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) ) )
144 136 143 mpd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> A. x e. ( { 0 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) )
145 iunss 
 |-  ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) <-> A. x e. ( { 0 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) )
146 144 145 sylibr 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) C_ ( dom R u. ran R ) )
147 102 ad2antll 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> A. x e. NN0 ran ( R ^r x ) C_ ( dom R u. ran R ) )
148 141 imim1d 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( x e. NN0 -> ran ( R ^r x ) C_ ( dom R u. ran R ) ) -> ( x e. ( { 0 } i^i Z ) -> ran ( R ^r x ) C_ ( dom R u. ran R ) ) ) )
149 148 ralimdv2 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( A. x e. NN0 ran ( R ^r x ) C_ ( dom R u. ran R ) -> A. x e. ( { 0 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) ) )
150 147 149 mpd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> A. x e. ( { 0 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) )
151 iunss 
 |-  ( U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) <-> A. x e. ( { 0 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) )
152 150 151 sylibr 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) C_ ( dom R u. ran R ) )
153 146 152 unssd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) C_ ( dom R u. ran R ) )
154 ssequn1 
 |-  ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) C_ ( dom R u. ran R ) <-> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( dom R u. ran R ) ) = ( dom R u. ran R ) )
155 153 154 sylib 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( dom R u. ran R ) ) = ( dom R u. ran R ) )
156 135 155 eqtrd 
 |-  ( ( 1 e. Z /\ ( Z C_ NN0 /\ R e. V ) ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
157 156 ex 
 |-  ( 1 e. Z -> ( ( Z C_ NN0 /\ R e. V ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) ) )
158 113 157 jaoi 
 |-  ( ( 0 e. Z \/ 1 e. Z ) -> ( ( Z C_ NN0 /\ R e. V ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) ) )
159 57 158 syl 
 |-  ( ( { 0 , 1 } i^i Z ) =/= (/) -> ( ( Z C_ NN0 /\ R e. V ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) ) )
160 159 3impib 
 |-  ( ( ( { 0 , 1 } i^i Z ) =/= (/) /\ Z C_ NN0 /\ R e. V ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
161 160 3com13 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
162 161 uneq1d 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) ) = ( ( dom R u. ran R ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) ) )
163 88 adantr 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> A. x e. NN0 dom ( R ^r x ) C_ ( dom R u. ran R ) )
164 ssel 
 |-  ( Z C_ NN0 -> ( x e. Z -> x e. NN0 ) )
165 164 adantl 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> ( x e. Z -> x e. NN0 ) )
166 165 imim1d 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> ( ( x e. NN0 -> dom ( R ^r x ) C_ ( dom R u. ran R ) ) -> ( x e. Z -> dom ( R ^r x ) C_ ( dom R u. ran R ) ) ) )
167 166 ralimdv2 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> ( A. x e. NN0 dom ( R ^r x ) C_ ( dom R u. ran R ) -> A. x e. Z dom ( R ^r x ) C_ ( dom R u. ran R ) ) )
168 163 167 mpd 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> A. x e. Z dom ( R ^r x ) C_ ( dom R u. ran R ) )
169 iunss 
 |-  ( U_ x e. Z dom ( R ^r x ) C_ ( dom R u. ran R ) <-> A. x e. Z dom ( R ^r x ) C_ ( dom R u. ran R ) )
170 168 169 sylibr 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> U_ x e. Z dom ( R ^r x ) C_ ( dom R u. ran R ) )
171 102 adantr 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> A. x e. NN0 ran ( R ^r x ) C_ ( dom R u. ran R ) )
172 165 imim1d 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> ( ( x e. NN0 -> ran ( R ^r x ) C_ ( dom R u. ran R ) ) -> ( x e. Z -> ran ( R ^r x ) C_ ( dom R u. ran R ) ) ) )
173 172 ralimdv2 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> ( A. x e. NN0 ran ( R ^r x ) C_ ( dom R u. ran R ) -> A. x e. Z ran ( R ^r x ) C_ ( dom R u. ran R ) ) )
174 171 173 mpd 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> A. x e. Z ran ( R ^r x ) C_ ( dom R u. ran R ) )
175 iunss 
 |-  ( U_ x e. Z ran ( R ^r x ) C_ ( dom R u. ran R ) <-> A. x e. Z ran ( R ^r x ) C_ ( dom R u. ran R ) )
176 174 175 sylibr 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> U_ x e. Z ran ( R ^r x ) C_ ( dom R u. ran R ) )
177 170 176 unssd 
 |-  ( ( R e. V /\ Z C_ NN0 ) -> ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) C_ ( dom R u. ran R ) )
178 177 3adant3 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) C_ ( dom R u. ran R ) )
179 ssequn2 
 |-  ( ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) C_ ( dom R u. ran R ) <-> ( ( dom R u. ran R ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
180 178 179 sylib 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( ( dom R u. ran R ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
181 162 180 eqtrd 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( ( ( U_ x e. ( { 0 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 0 } i^i Z ) ran ( R ^r x ) ) u. ( U_ x e. ( { 1 } i^i Z ) dom ( R ^r x ) u. U_ x e. ( { 1 } i^i Z ) ran ( R ^r x ) ) ) u. ( U_ x e. Z dom ( R ^r x ) u. U_ x e. Z ran ( R ^r x ) ) ) = ( dom R u. ran R ) )
182 35 181 syl5eq 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( dom U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) u. ran U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ) = ( dom R u. ran R ) )
183 nn0ex 
 |-  NN0 e. _V
184 183 ssex 
 |-  ( Z C_ NN0 -> Z e. _V )
185 incom 
 |-  ( Z i^i { 0 } ) = ( { 0 } i^i Z )
186 inex1g 
 |-  ( Z e. _V -> ( Z i^i { 0 } ) e. _V )
187 185 186 eqeltrrid 
 |-  ( Z e. _V -> ( { 0 } i^i Z ) e. _V )
188 incom 
 |-  ( Z i^i { 1 } ) = ( { 1 } i^i Z )
189 inex1g 
 |-  ( Z e. _V -> ( Z i^i { 1 } ) e. _V )
190 188 189 eqeltrrid 
 |-  ( Z e. _V -> ( { 1 } i^i Z ) e. _V )
191 unexg 
 |-  ( ( ( { 0 } i^i Z ) e. _V /\ ( { 1 } i^i Z ) e. _V ) -> ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) e. _V )
192 187 190 191 syl2anc 
 |-  ( Z e. _V -> ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) e. _V )
193 unexg 
 |-  ( ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) e. _V /\ Z e. _V ) -> ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) e. _V )
194 192 193 mpancom 
 |-  ( Z e. _V -> ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) e. _V )
195 ovex 
 |-  ( R ^r x ) e. _V
196 195 rgenw 
 |-  A. x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) e. _V
197 iunexg 
 |-  ( ( ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) e. _V /\ A. x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) e. _V ) -> U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) e. _V )
198 194 196 197 sylancl 
 |-  ( Z e. _V -> U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) e. _V )
199 184 198 syl 
 |-  ( Z C_ NN0 -> U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) e. _V )
200 199 3ad2ant2 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) e. _V )
201 simp1 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> R e. V )
202 relexp0eq 
 |-  ( ( U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) e. _V /\ R e. V ) -> ( ( dom U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) u. ran U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ) = ( dom R u. ran R ) <-> ( U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ^r 0 ) = ( R ^r 0 ) ) )
203 200 201 202 syl2anc 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( ( dom U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) u. ran U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ) = ( dom R u. ran R ) <-> ( U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ^r 0 ) = ( R ^r 0 ) ) )
204 182 203 mpbid 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( U_ x e. ( ( ( { 0 } i^i Z ) u. ( { 1 } i^i Z ) ) u. Z ) ( R ^r x ) ^r 0 ) = ( R ^r 0 ) )
205 12 204 syl5eq 
 |-  ( ( R e. V /\ Z C_ NN0 /\ ( { 0 , 1 } i^i Z ) =/= (/) ) -> ( U_ x e. Z ( R ^r x ) ^r 0 ) = ( R ^r 0 ) )