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 ( ( 𝑅 ∈ 𝑉 ∧ 𝑍 ⊆ ℕ0 ∧ ( { 0 , 1 } ∩ 𝑍 ) ≠ ∅ ) → ( ∪ 𝑥 ∈ 𝑍 ( 𝑅 ↑𝑟 𝑥 ) ↑𝑟 0 ) = ( 𝑅 ↑𝑟 0 ) )

Proof

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