Theorem relexp0g 14375

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 2822	. . 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 771	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 0)) → 𝑛 = 0)
3	2	iftrued 4474	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑟 ∪ ran 𝑟)))
4		dmeq 5766	. . . . . . 7 ⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
5		rneq 5800	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
6	4, 5	uneq12d 4139	. . . . . 6 ⊢ (𝑟 = 𝑅 → (dom 𝑟 ∪ ran 𝑟) = (dom 𝑅 ∪ ran 𝑅))
7	6	reseq2d 5847	. . . . 5 ⊢ (𝑟 = 𝑅 → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
8	7	ad2antrl 726	. . . 4 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 0)) → ( I ↾ (dom 𝑟 ∪ ran 𝑟)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
9	3, 8	eqtrd 2856	. . 3 ⊢ ((𝑅 ∈ 𝑉 ∧ (𝑟 = 𝑅 ∧ 𝑛 = 0)) → if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
10		elex 3512	. . 3 ⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V)
11		0nn0 11906	. . . 4 ⊢ 0 ∈ ℕ0
12	11	a1i 11	. . 3 ⊢ (𝑅 ∈ 𝑉 → 0 ∈ ℕ0)
13		dmexg 7607	. . . . 5 ⊢ (𝑅 ∈ 𝑉 → dom 𝑅 ∈ V)
14		rnexg 7608	. . . . 5 ⊢ (𝑅 ∈ 𝑉 → ran 𝑅 ∈ V)
15		unexg 7466	. . . . 5 ⊢ ((dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V) → (dom 𝑅 ∪ ran 𝑅) ∈ V)
16	13, 14, 15	syl2anc 586	. . . 4 ⊢ (𝑅 ∈ 𝑉 → (dom 𝑅 ∪ ran 𝑅) ∈ V)
17		resiexg 7613	. . . 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 7296	. 2 ⊢ (𝑅 ∈ 𝑉 → (𝑅(𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))
20		df-relexp 14374	. . 3 ⊢ ↑𝑟 = (𝑟 ∈ V, 𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( I ↾ (dom 𝑟 ∪ ran 𝑟)), (seq1((𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑥 ∘ 𝑟)), (𝑧 ∈ V ↦ 𝑟))‘𝑛)))
21		oveq 7156	. . . . 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 2823	. . . 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 343	. . 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 233	1 ⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟0) = ( I ↾ (dom 𝑅 ∪ ran 𝑅)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  Vcvv 3494   ∪ cun 3933  ifcif 4466   ↦ cmpt 5138   I cid 5453  dom cdm 5549  ran crn 5550   ↾ cres 5551   ∘ ccom 5553  ‘cfv 6349  (class class class)co 7150   ∈ cmpo 7152  0cc0 10531  1c1 10532  ℕ₀cn0 11891  seqcseq 13363  ↑_𝑟crelexp 14373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-mulcl 10593  ax-i2m1 10599

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-iota 6308  df-fun 6351  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-n0 11892  df-relexp 14374

This theorem is referenced by:  relexp0  14376  relexpcnv  14388  relexp0rel  14390  relexpdmg  14395  relexprng  14399  relexpfld  14402  relexpaddg  14406  dfrcl3  40013  fvmptiunrelexplb0d  40022  brfvrcld2  40030  relexp0eq  40039  iunrelexp0  40040  relexpiidm  40042  relexpss1d  40043  relexpmulg  40048  iunrelexpmin2  40050  relexp01min  40051  relexp0a  40054  relexpxpmin  40055  relexpaddss  40056  dfrtrcl3  40071  cotrclrcl  40080