MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  relexp0g Structured version   Visualization version   GIF version

Theorem relexp0g 14973
Description: A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
Assertion
Ref Expression
relexp0g (𝑅𝑉 → (𝑅𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))

Proof of Theorem relexp0g
Dummy variables 𝑛 𝑟 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqidd 2731 . . 3 (𝑅𝑉 → (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛))) = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛))))
2 simprr 769 . . . . 5 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → 𝑛 = 0)
32iftrued 4535 . . . 4 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑟 ∪ ran 𝑟)))
4 dmeq 5902 . . . . . . 7 (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
5 rneq 5934 . . . . . . 7 (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
64, 5uneq12d 4163 . . . . . 6 (𝑟 = 𝑅 → (dom 𝑟 ∪ ran 𝑟) = (dom 𝑅 ∪ ran 𝑅))
76reseq2d 5980 . . . . 5 (𝑟 = 𝑅 → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
87ad2antrl 724 . . . 4 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
93, 8eqtrd 2770 . . 3 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
10 elex 3491 . . 3 (𝑅𝑉𝑅 ∈ V)
11 0nn0 12491 . . . 4 0 ∈ ℕ0
1211a1i 11 . . 3 (𝑅𝑉 → 0 ∈ ℕ0)
13 dmexg 7896 . . . . 5 (𝑅𝑉 → dom 𝑅 ∈ V)
14 rnexg 7897 . . . . 5 (𝑅𝑉 → ran 𝑅 ∈ V)
15 unexg 7738 . . . . 5 ((dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V)
1613, 14, 15syl2anc 582 . . . 4 (𝑅𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V)
17 resiexg 7907 . . . 4 ((dom 𝑅 ∪ ran 𝑅) ∈ V → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V)
1816, 17syl 17 . . 3 (𝑅𝑉 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V)
191, 9, 10, 12, 18ovmpod 7562 . 2 (𝑅𝑉 → (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
20 df-relexp 14971 . . 3 𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
21 oveq 7417 . . . . 5 (↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛))) → (𝑅𝑟0) = (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0))
2221eqeq1d 2732 . . . 4 (↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛))) → ((𝑅𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ↔ (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))))
2322imbi2d 339 . . 3 (↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛))) → ((𝑅𝑉 → (𝑅𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) ↔ (𝑅𝑉 → (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))))
2420, 23ax-mp 5 . 2 ((𝑅𝑉 → (𝑅𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) ↔ (𝑅𝑉 → (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))))
2519, 24mpbir 230 1 (𝑅𝑉 → (𝑅𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1539  wcel 2104  Vcvv 3472  cun 3945  ifcif 4527  cmpt 5230   I cid 5572  dom cdm 5675  ran crn 5676  cres 5677  ccom 5679  cfv 6542  (class class class)co 7411  cmpo 7413  0cc0 11112  1c1 11113  0cn0 12476  seqcseq 13970  𝑟crelexp 14970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-i2m1 11180
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-iota 6494  df-fun 6544  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-n0 12477  df-relexp 14971
This theorem is referenced by:  relexp0  14974  relexpcnv  14986  relexp0rel  14988  relexpdmg  14993  relexprng  14997  relexpfld  15000  relexpaddg  15004  dfrcl3  42728  fvmptiunrelexplb0d  42737  brfvrcld2  42745  relexp0eq  42754  iunrelexp0  42755  relexpiidm  42757  relexpss1d  42758  relexpmulg  42763  iunrelexpmin2  42765  relexp01min  42766  relexp0a  42769  relexpxpmin  42770  relexpaddss  42771  dfrtrcl3  42786  cotrclrcl  42795
  Copyright terms: Public domain W3C validator