Metamath Proof Explorer

Theorem relexp0a

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

Ref Expression
Assertion relexp0a ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 oveq2 ⊢ ( 𝑥 = 1 → ( 𝐴 ↑𝑟 𝑥 ) = ( 𝐴 ↑𝑟 1 ) )
3 2 oveq1d ⊢ ( 𝑥 = 1 → ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) = ( ( 𝐴 ↑𝑟 1 ) ↑𝑟 0 ) )
4 3 sseq1d ⊢ ( 𝑥 = 1 → ( ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ↔ ( ( 𝐴 ↑𝑟 1 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) )
5 4 imbi2d ⊢ ( 𝑥 = 1 → ( ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ↔ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 1 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ) )
6 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑𝑟 𝑥 ) = ( 𝐴 ↑𝑟 𝑦 ) )
7 6 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) = ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) )
8 7 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ↔ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) )
9 8 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ↔ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ) )
10 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐴 ↑𝑟 𝑥 ) = ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) )
11 10 oveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) = ( ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ↑𝑟 0 ) )
12 11 sseq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ↔ ( ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) )
13 12 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ↔ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ) )
14 oveq2 ⊢ ( 𝑥 = 𝑁 → ( 𝐴 ↑𝑟 𝑥 ) = ( 𝐴 ↑𝑟 𝑁 ) )
15 14 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) = ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) )
16 15 sseq1d ⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ↔ ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) )
17 16 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑥 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ↔ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ) )
18 relexp1g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑𝑟 1 ) = 𝐴 )
19 18 oveq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 1 ) ↑𝑟 0 ) = ( 𝐴 ↑𝑟 0 ) )
20 ssid ⊢ ( 𝐴 ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 )
21 19 20 eqsstrdi ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 1 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) )
22 simp2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → 𝐴 ∈ 𝑉 )
23 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → 𝑦 ∈ ℕ )
24 relexpsucnnr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ ) → ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) = ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) )
25 24 oveq1d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑦 ∈ ℕ ) → ( ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ↑𝑟 0 ) = ( ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ↑𝑟 0 ) )
26 22 23 25 syl2anc ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ↑𝑟 0 ) = ( ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ↑𝑟 0 ) )
27 ovex ⊢ ( 𝐴 ↑𝑟 𝑦 ) ∈ V
28 coexg ⊢ ( ( ( 𝐴 ↑𝑟 𝑦 ) ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∈ V )
29 27 28 mpan ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∈ V )
30 relexp0g ⊢ ( ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∈ V → ( ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ↑𝑟 0 ) = ( I ↾ ( dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∪ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ) ) )
31 29 30 syl ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ↑𝑟 0 ) = ( I ↾ ( dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∪ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ) ) )
32 dmcoss ⊢ dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ⊆ dom 𝐴
33 rncoss ⊢ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ⊆ ran ( 𝐴 ↑𝑟 𝑦 )
34 unss12 ⊢ ( ( dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ⊆ dom 𝐴 ∧ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ⊆ ran ( 𝐴 ↑𝑟 𝑦 ) ) → ( dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∪ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) )
35 32 33 34 mp2an ⊢ ( dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∪ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) )
36 ssres2 ⊢ ( ( dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∪ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ) ⊆ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) → ( I ↾ ( dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∪ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ) ) ⊆ ( I ↾ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) )
37 35 36 ax-mp ⊢ ( I ↾ ( dom ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ∪ ran ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ) ) ⊆ ( I ↾ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) )
38 31 37 eqsstrdi ⊢ ( 𝐴 ∈ 𝑉 → ( ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ↑𝑟 0 ) ⊆ ( I ↾ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) )
39 22 38 syl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ↑𝑟 0 ) ⊆ ( I ↾ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) )
40 resundi ⊢ ( I ↾ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) = ( ( I ↾ dom 𝐴 ) ∪ ( I ↾ ran ( 𝐴 ↑𝑟 𝑦 ) ) )
41 ssun1 ⊢ dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
42 ssres2 ⊢ ( dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) → ( I ↾ dom 𝐴 ) ⊆ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
43 41 42 ax-mp ⊢ ( I ↾ dom 𝐴 ) ⊆ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) )
44 relexp0g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑𝑟 0 ) = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
45 43 44 sseqtrrid ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ dom 𝐴 ) ⊆ ( 𝐴 ↑𝑟 0 ) )
46 45 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( I ↾ dom 𝐴 ) ⊆ ( 𝐴 ↑𝑟 0 ) )
47 ssun2 ⊢ ran ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( dom ( 𝐴 ↑𝑟 𝑦 ) ∪ ran ( 𝐴 ↑𝑟 𝑦 ) )
48 ssres2 ⊢ ( ran ( 𝐴 ↑𝑟 𝑦 ) ⊆ ( dom ( 𝐴 ↑𝑟 𝑦 ) ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) → ( I ↾ ran ( 𝐴 ↑𝑟 𝑦 ) ) ⊆ ( I ↾ ( dom ( 𝐴 ↑𝑟 𝑦 ) ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) )
49 47 48 ax-mp ⊢ ( I ↾ ran ( 𝐴 ↑𝑟 𝑦 ) ) ⊆ ( I ↾ ( dom ( 𝐴 ↑𝑟 𝑦 ) ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) )
50 relexp0g ⊢ ( ( 𝐴 ↑𝑟 𝑦 ) ∈ V → ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) = ( I ↾ ( dom ( 𝐴 ↑𝑟 𝑦 ) ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) )
51 27 50 ax-mp ⊢ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) = ( I ↾ ( dom ( 𝐴 ↑𝑟 𝑦 ) ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) )
52 49 51 sseqtrri ⊢ ( I ↾ ran ( 𝐴 ↑𝑟 𝑦 ) ) ⊆ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 )
53 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) )
54 52 53 sstrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( I ↾ ran ( 𝐴 ↑𝑟 𝑦 ) ) ⊆ ( 𝐴 ↑𝑟 0 ) )
55 46 54 unssd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( ( I ↾ dom 𝐴 ) ∪ ( I ↾ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) ⊆ ( 𝐴 ↑𝑟 0 ) )
56 40 55 eqsstrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( I ↾ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) ⊆ ( 𝐴 ↑𝑟 0 ) )
57 56 3adant1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( I ↾ ( dom 𝐴 ∪ ran ( 𝐴 ↑𝑟 𝑦 ) ) ) ⊆ ( 𝐴 ↑𝑟 0 ) )
58 39 57 sstrd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( ( ( 𝐴 ↑𝑟 𝑦 ) ∘ 𝐴 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) )
59 26 58 eqsstrd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐴 ∈ 𝑉 ∧ ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) )
60 59 3exp ⊢ ( 𝑦 ∈ ℕ → ( 𝐴 ∈ 𝑉 → ( ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) → ( ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ) )
61 60 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑦 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) → ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 ( 𝑦 + 1 ) ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) ) )
62 5 9 13 17 21 61 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) )
63 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐴 ↑𝑟 𝑁 ) = ( 𝐴 ↑𝑟 0 ) )
64 63 oveq1d ⊢ ( 𝑁 = 0 → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) = ( ( 𝐴 ↑𝑟 0 ) ↑𝑟 0 ) )
65 relexp0idm ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 0 ) ↑𝑟 0 ) = ( 𝐴 ↑𝑟 0 ) )
66 64 65 sylan9eq ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) = ( 𝐴 ↑𝑟 0 ) )
67 eqimss ⊢ ( ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) = ( 𝐴 ↑𝑟 0 ) → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) )
68 66 67 syl ⊢ ( ( 𝑁 = 0 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) )
69 68 ex ⊢ ( 𝑁 = 0 → ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) )
70 62 69 jaoi ⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) )
71 1 70 sylbi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) ) )
72 71 impcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ↑𝑟 𝑁 ) ↑𝑟 0 ) ⊆ ( 𝐴 ↑𝑟 0 ) )