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

Theorem relexp0g 15057
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 2735 . . 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 773 . . . . 5 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → 𝑛 = 0)
32iftrued 4538 . . . 4 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑟 ∪ ran 𝑟)))
4 dmeq 5916 . . . . . . 7 (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
5 rneq 5949 . . . . . . 7 (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
64, 5uneq12d 4178 . . . . . 6 (𝑟 = 𝑅 → (dom 𝑟 ∪ ran 𝑟) = (dom 𝑅 ∪ ran 𝑅))
76reseq2d 5999 . . . . 5 (𝑟 = 𝑅 → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
87ad2antrl 728 . . . 4 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
93, 8eqtrd 2774 . . 3 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
10 elex 3498 . . 3 (𝑅𝑉𝑅 ∈ V)
11 0nn0 12538 . . . 4 0 ∈ ℕ0
1211a1i 11 . . 3 (𝑅𝑉 → 0 ∈ ℕ0)
13 dmexg 7923 . . . . 5 (𝑅𝑉 → dom 𝑅 ∈ V)
14 rnexg 7924 . . . . 5 (𝑅𝑉 → ran 𝑅 ∈ V)
15 unexg 7761 . . . . 5 ((dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V)
1613, 14, 15syl2anc 584 . . . 4 (𝑅𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V)
17 resiexg 7934 . . . 4 ((dom 𝑅 ∪ ran 𝑅) ∈ V → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V)
1816, 17syl 17 . . 3 (𝑅𝑉 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V)
191, 9, 10, 12, 18ovmpod 7584 . 2 (𝑅𝑉 → (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
20 df-relexp 15055 . . 3 𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
21 oveq 7436 . . . . 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 2736 . . . 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 340 . . 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 231 1 (𝑅𝑉 → (𝑅𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  Vcvv 3477  cun 3960  ifcif 4530  cmpt 5230   I cid 5581  dom cdm 5688  ran crn 5689  cres 5690  ccom 5692  cfv 6562  (class class class)co 7430  cmpo 7432  0cc0 11152  1c1 11153  0cn0 12523  seqcseq 14038  𝑟crelexp 15054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-i2m1 11220
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-iota 6515  df-fun 6564  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-n0 12524  df-relexp 15055
This theorem is referenced by:  relexp0  15058  relexpcnv  15070  relexp0rel  15072  relexpdmg  15077  relexprng  15081  relexpfld  15084  relexpaddg  15088  dfrcl3  43664  fvmptiunrelexplb0d  43673  brfvrcld2  43681  relexp0eq  43690  iunrelexp0  43691  relexpiidm  43693  relexpss1d  43694  relexpmulg  43699  iunrelexpmin2  43701  relexp01min  43702  relexp0a  43705  relexpxpmin  43706  relexpaddss  43707  dfrtrcl3  43722  cotrclrcl  43731
  Copyright terms: Public domain W3C validator