Theorem dmtrclfv 13093

Description: The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 9-May-2020.)

Assertion

Ref	Expression
dmtrclfv	|- ( R e. V -> dom ( t+ ` R ) = dom R )

Proof of Theorem dmtrclfv

Step	Hyp	Ref	Expression
1		trclfvub 13082	. . . 4 |- ( R e. V -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )
2		dmss 5012	. . . 4 |- ( ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) -> dom ( t+ ` R ) C_ dom ( R u. ( dom R X. ran R ) ) )
3	1, 2	syl 17	. . 3 |- ( R e. V -> dom ( t+ ` R ) C_ dom ( R u. ( dom R X. ran R ) ) )
4		dmun 5019	. . . 4 |- dom ( R u. ( dom R X. ran R ) ) = ( dom R u. dom ( dom R X. ran R ) )
5		dm0rn0 5029	. . . . . . 7 |- ( dom R = (/) <-> ran R = (/) )
6		xpeq1 4826	. . . . . . . . . 10 |- ( dom R = (/) -> ( dom R X. ran R ) = ( (/) X. ran R ) )
7		0xp 4893	. . . . . . . . . 10 |- ( (/) X. ran R ) = (/)
8	6, 7	syl6eq 2502	. . . . . . . . 9 |- ( dom R = (/) -> ( dom R X. ran R ) = (/) )
9	8	dmeqd 5015	. . . . . . . 8 |- ( dom R = (/) -> dom ( dom R X. ran R ) = dom (/) )
10		dm0 5026	. . . . . . . . 9 |- dom (/) = (/)
11	10	a1i 11	. . . . . . . 8 |- ( dom R = (/) -> dom (/) = (/) )
12		eqcom 2459	. . . . . . . . 9 |- ( dom R = (/) <-> (/) = dom R )
13	12	biimpi 199	. . . . . . . 8 |- ( dom R = (/) -> (/) = dom R )
14	9, 11, 13	3eqtrd 2490	. . . . . . 7 |- ( dom R = (/) -> dom ( dom R X. ran R ) = dom R )
15	5, 14	sylbir 218	. . . . . 6 |- ( ran R = (/) -> dom ( dom R X. ran R ) = dom R )
16		dmxp 5031	. . . . . 6 |- ( ran R =/= (/) -> dom ( dom R X. ran R ) = dom R )
17	15, 16	pm2.61ine 2707	. . . . 5 |- dom ( dom R X. ran R ) = dom R
18	17	uneq2i 3553	. . . 4 |- ( dom R u. dom ( dom R X. ran R ) ) = ( dom R u. dom R )
19		unidm 3545	. . . 4 |- ( dom R u. dom R ) = dom R
20	4, 18, 19	3eqtri 2478	. . 3 |- dom ( R u. ( dom R X. ran R ) ) = dom R
21	3, 20	syl6sseq 3446	. 2 |- ( R e. V -> dom ( t+ ` R ) C_ dom R )
22		trclfvlb 13083	. . 3 |- ( R e. V -> R C_ ( t+ ` R ) )
23		dmss 5012	. . 3 |- ( R C_ ( t+ ` R ) -> dom R C_ dom ( t+ ` R ) )
24	22, 23	syl 17	. 2 |- ( R e. V -> dom R C_ dom ( t+ ` R ) )
25	21, 24	eqssd 3417	1 |- ( R e. V -> dom ( t+ ` R ) = dom R )

Syntax hints:   -> wi 4   = wceq 1448   e. wcel 1891   u. cun 3370   C_ wss 3372   (/)c0 3699   X. cxp 4810   dom cdm 4812   ran crn 4813   ` cfv 5561   t+ctcl 13060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-sbc 3236  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4169  df-int 4205  df-br 4375  df-opab 4434  df-mpt 4435  df-id 4727  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-iota 5525  df-fun 5563  df-fv 5569  df-trcl 13062

This theorem is referenced by:  rntrclfvRP  36325