Metamath Proof Explorer


Theorem rclexi

Description: The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020)

Ref Expression
Hypothesis rclexi.1 AV
Assertion rclexi x|AxIdomxranxxV

Proof

Step Hyp Ref Expression
1 rclexi.1 AV
2 ssun1 AAIdomAranA
3 dmun domAIdomAranA=domAdomIdomAranA
4 dmresi domIdomAranA=domAranA
5 4 uneq2i domAdomIdomAranA=domAdomAranA
6 ssun1 domAdomAranA
7 ssequn1 domAdomAranAdomAdomAranA=domAranA
8 6 7 mpbi domAdomAranA=domAranA
9 3 5 8 3eqtri domAIdomAranA=domAranA
10 rnun ranAIdomAranA=ranAranIdomAranA
11 rnresi ranIdomAranA=domAranA
12 11 uneq2i ranAranIdomAranA=ranAdomAranA
13 ssun2 ranAdomAranA
14 ssequn1 ranAdomAranAranAdomAranA=domAranA
15 13 14 mpbi ranAdomAranA=domAranA
16 10 12 15 3eqtri ranAIdomAranA=domAranA
17 9 16 uneq12i domAIdomAranAranAIdomAranA=domAranAdomAranA
18 unidm domAranAdomAranA=domAranA
19 17 18 eqtri domAIdomAranAranAIdomAranA=domAranA
20 19 reseq2i IdomAIdomAranAranAIdomAranA=IdomAranA
21 ssun2 IdomAranAAIdomAranA
22 20 21 eqsstri IdomAIdomAranAranAIdomAranAAIdomAranA
23 1 elexi AV
24 dmexg AVdomAV
25 rnexg AVranAV
26 24 25 unexd AVdomAranAV
27 26 resiexd AVIdomAranAV
28 1 27 ax-mp IdomAranAV
29 23 28 unex AIdomAranAV
30 dmeq x=AIdomAranAdomx=domAIdomAranA
31 rneq x=AIdomAranAranx=ranAIdomAranA
32 30 31 uneq12d x=AIdomAranAdomxranx=domAIdomAranAranAIdomAranA
33 32 reseq2d x=AIdomAranAIdomxranx=IdomAIdomAranAranAIdomAranA
34 id x=AIdomAranAx=AIdomAranA
35 33 34 sseq12d x=AIdomAranAIdomxranxxIdomAIdomAranAranAIdomAranAAIdomAranA
36 35 cleq2lem x=AIdomAranAAxIdomxranxxAAIdomAranAIdomAIdomAranAranAIdomAranAAIdomAranA
37 29 36 spcev AAIdomAranAIdomAIdomAranAranAIdomAranAAIdomAranAxAxIdomxranxx
38 intexab xAxIdomxranxxx|AxIdomxranxxV
39 37 38 sylib AAIdomAranAIdomAIdomAranAranAIdomAranAAIdomAranAx|AxIdomxranxxV
40 2 22 39 mp2an x|AxIdomxranxxV