Theorem relexp0g 15041

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.

Step	Hyp	Ref	Expression
1		eqidd 2736	. . 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 772	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 0)) → 𝑛 = 0)
3	2	iftrued 4508	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑟 ∪ ran 𝑟)))
4		dmeq 5883	. . . . . . 7 ⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
5		rneq 5916	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
6	4, 5	uneq12d 4144	. . . . . 6 ⊢ (𝑟 = 𝑅 → (dom 𝑟 ∪ ran 𝑟) = (dom 𝑅 ∪ ran 𝑅))
7	6	reseq2d 5966	. . . . 5 ⊢ (𝑟 = 𝑅 → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
8	7	ad2antrl 728	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 0)) → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
9	3, 8	eqtrd 2770	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
10		elex 3480	. . 3 ⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V)
11		0nn0 12516	. . . 4 ⊢ 0 ∈ ℕ0
12	11	a1i 11	. . 3 ⊢ (𝑅 ∈ 𝑉 → 0 ∈ ℕ0)
13		dmexg 7897	. . . . 5 ⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V)
14		rnexg 7898	. . . . 5 ⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V)
15		unexg 7737	. . . . 5 ⊢ ((dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V)
16	13, 14, 15	syl2anc 584	. . . 4 ⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V)
17		resiexg 7908	. . . 4 ⊢ ((dom 𝑅 ∪ ran 𝑅) ∈ V → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V)
18	16, 17	syl 17	. . 3 ⊢ (𝑅 ∈ 𝑉 → ( I ↾ (dom 𝑅 ∪ ran 𝑅)) ∈ V)
19	1, 9, 10, 12, 18	ovmpod 7559	. 2 ⊢ (𝑅 ∈ 𝑉 → (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
20		df-relexp 15039	. . 3 ⊢ ↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
21		oveq 7411	. . . . 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))
22	21	eqeq1d 2737	. . . 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 𝑅))))
23	22	imbi2d 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 𝑅)))))
24	20, 23	ax-mp 5	. 2 ⊢ ((𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))) ↔ (𝑅 ∈ 𝑉 → (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅))))
25	19, 24	mpbir 231	1 ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ∪ cun 3924  ifcif 4500   ↦ cmpt 5201   I cid 5547  dom cdm 5654  ran crn 5655   ↾ cres 5656   ∘ ccom 5658  ‘cfv 6531  (class class class)co 7405   ∈ cmpo 7407  0cc0 11129  1c1 11130  ℕ₀cn0 12501  seqcseq 14019  ↑_𝑟crelexp 15038

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-mulcl 11191  ax-i2m1 11197

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-n0 12502  df-relexp 15039

This theorem is referenced by:  relexp0  15042  relexpcnv  15054  relexp0rel  15056  relexpdmg  15061  relexprng  15065  relexpfld  15068  relexpaddg  15072  dfrcl3  43699  fvmptiunrelexplb0d  43708  brfvrcld2  43716  relexp0eq  43725  iunrelexp0  43726  relexpiidm  43728  relexpss1d  43729  relexpmulg  43734  iunrelexpmin2  43736  relexp01min  43737  relexp0a  43740  relexpxpmin  43741  relexpaddss  43742  dfrtrcl3  43757  cotrclrcl  43766