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

Theorem relexp0g 14139
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 2826 . . 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 789 . . . . 5 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → 𝑛 = 0)
32iftrued 4314 . . . 4 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑟 ∪ ran 𝑟)))
4 dmeq 5556 . . . . . . 7 (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
5 rneq 5583 . . . . . . 7 (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
64, 5uneq12d 3995 . . . . . 6 (𝑟 = 𝑅 → (dom 𝑟 ∪ ran 𝑟) = (dom 𝑅 ∪ ran 𝑅))
76reseq2d 5629 . . . . 5 (𝑟 = 𝑅 → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
87ad2antrl 719 . . . 4 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
93, 8eqtrd 2861 . . 3 ((𝑅𝑉 ∧ (𝑟 = 𝑅𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
10 elex 3429 . . 3 (𝑅𝑉𝑅 ∈ V)
11 0nn0 11635 . . . 4 0 ∈ ℕ0
1211a1i 11 . . 3 (𝑅𝑉 → 0 ∈ ℕ0)
13 dmexg 7358 . . . . 5 (𝑅𝑉 → dom 𝑅 ∈ V)
14 rnexg 7359 . . . . 5 (𝑅𝑉 → ran 𝑅 ∈ V)
15 unexg 7219 . . . . 5 ((dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V)
1613, 14, 15syl2anc 579 . . . 4 (𝑅𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V)
17 resiexg 7364 . . . 4 ((dom 𝑅 ∪ ran 𝑅) ∈ V → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V)
1816, 17syl 17 . . 3 (𝑅𝑉 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V)
191, 9, 10, 12, 18ovmpt2d 7048 . 2 (𝑅𝑉 → (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
20 df-relexp 14138 . . 3 𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
21 oveq 6911 . . . . 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 2827 . . . 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 332 . . 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 223 1 (𝑅𝑉 → (𝑅𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1656  wcel 2164  Vcvv 3414  cun 3796  ifcif 4306  cmpt 4952   I cid 5249  dom cdm 5342  ran crn 5343  cres 5344  ccom 5346  cfv 6123  (class class class)co 6905  cmpt2 6907  0cc0 10252  1c1 10253  0cn0 11618  seqcseq 13095  𝑟crelexp 14137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-mulcl 10314  ax-i2m1 10320
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-iota 6086  df-fun 6125  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-n0 11619  df-relexp 14138
This theorem is referenced by:  relexp0  14140  relexpcnv  14152  relexp0rel  14154  relexpdmg  14159  relexprng  14163  relexpfld  14166  relexpaddg  14170  dfrcl3  38801  fvmptiunrelexplb0d  38810  brfvrcld2  38818  relexp0eq  38827  iunrelexp0  38828  relexpiidm  38830  relexpss1d  38831  relexpmulg  38836  iunrelexpmin2  38838  relexp01min  38839  relexp0a  38842  relexpxpmin  38843  relexpaddss  38844  dfrtrcl3  38859  cotrclrcl  38868
  Copyright terms: Public domain W3C validator