| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > relexp1g | Structured version Visualization version GIF version | ||
| Description: A relation composed once is itself. (Contributed by RP, 22-May-2020.) |
| Ref | Expression |
|---|---|
| relexp1g | ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-relexp 15033 | . . 3 ⊢ ↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛))) | |
| 2 | 1 | a1i 11 | . 2 ⊢ (𝑅 ∈ 𝑉 → ↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))) |
| 3 | simprr 782 | . . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → 𝑛 = 1) | |
| 4 | ax-1ne0 11142 | . . . . . . 7 ⊢ 1 ≠ 0 | |
| 5 | neeq1 3019 | . . . . . . 7 ⊢ (𝑛 = 1 → (𝑛 ≠ 0 ↔ 1 ≠ 0)) | |
| 6 | 4, 5 | mpbiri 260 | . . . . . 6 ⊢ (𝑛 = 1 → 𝑛 ≠ 0) |
| 7 | 3, 6 | syl 17 | . . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → 𝑛 ≠ 0) |
| 8 | 7 | neneqd 2962 | . . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → ¬ 𝑛 = 0) |
| 9 | 8 | iffalsed 4491 | . . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) |
| 10 | simprl 780 | . . . . . 6 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → 𝑟 = 𝑅) | |
| 11 | 10 | mpteq2dv 5194 | . . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → (𝑧 ∈ V ↦ 𝑟) = (𝑧 ∈ V ↦ 𝑅)) |
| 12 | 11 | seqeq3d 14022 | . . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟)) = seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑅))) |
| 13 | 12, 3 | fveq12d 6874 | . . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛) = (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑅))‘1)) |
| 14 | 1z 12601 | . . . 4 ⊢ 1 ∈ ℤ | |
| 15 | eqidd 2763 | . . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → (𝑧 ∈ V ↦ 𝑅) = (𝑧 ∈ V ↦ 𝑅)) | |
| 16 | eqidd 2763 | . . . . 5 ⊢ (((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) ∧ 𝑧 = 1) → 𝑅 = 𝑅) | |
| 17 | 1ex 11176 | . . . . . 6 ⊢ 1 ∈ V | |
| 18 | 17 | a1i 11 | . . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → 1 ∈ V) |
| 19 | simpl 486 | . . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → 𝑅 ∈ 𝑉) | |
| 20 | 15, 16, 18, 19 | fvmptd 6983 | . . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → ((𝑧 ∈ V ↦ 𝑅)‘1) = 𝑅) |
| 21 | 14, 20 | seq1i 14028 | . . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑅))‘1) = 𝑅) |
| 22 | 9, 13, 21 | 3eqtrd 2801 | . 2 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 1)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = 𝑅) |
| 23 | elex 3475 | . 2 ⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) | |
| 24 | 1nn0 12497 | . . 3 ⊢ 1 ∈ ℕ0 | |
| 25 | 24 | a1i 11 | . 2 ⊢ (𝑅 ∈ 𝑉 → 1 ∈ ℕ0) |
| 26 | 2, 22, 23, 25, 23 | ovmpod 7548 | 1 ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 399 = wceq 1560 ∈ wcel 2142 ≠ wne 2957 Vcvv 3454 ∪ cun 3902 ifcif 4480 ↦ cmpt 5181 I cid 5541 dom cdm 5647 ran crn 5648 ↾ cres 5649 ∘ ccom 5651 ‘cfv 6521 (class class class)co 7396 ∈ cmpo 7398 0cc0 11073 1c1 11074 ℕ0cn0 12481 seqcseq 14014 ↑𝑟crelexp 15032 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-er 8678 df-en 8928 df-dom 8929 df-sdom 8930 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-nn 12211 df-n0 12482 df-z 12569 df-uz 12840 df-seq 14015 df-relexp 15033 |
| This theorem is referenced by: dfid5 15040 dfid6 15041 relexp1d 15042 relexpsucnnl 15043 relexpsucl 15044 relexpsucr 15045 relexpcnv 15048 relexprelg 15051 relexpnndm 15054 relexpfld 15062 relexpaddnn 15064 relexpaddg 15066 dfrcl3 44248 relexp2 44250 iunrelexp0 44275 relexpxpnnidm 44276 corclrcl 44280 iunrelexpmin1 44281 trclrelexplem 44284 iunrelexpmin2 44285 relexp01min 44286 relexp0a 44289 relexpaddss 44291 dftrcl3 44293 cotrcltrcl 44298 trclimalb2 44299 trclfvdecomr 44301 dfrtrcl3 44306 corcltrcl 44312 cotrclrcl 44315 |
| Copyright terms: Public domain | W3C validator |