Description: The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rclexi.1 | |
|
Assertion | rclexi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rclexi.1 | |
|
2 | ssun1 | |
|
3 | dmun | |
|
4 | dmresi | |
|
5 | 4 | uneq2i | |
6 | ssun1 | |
|
7 | ssequn1 | |
|
8 | 6 7 | mpbi | |
9 | 3 5 8 | 3eqtri | |
10 | rnun | |
|
11 | rnresi | |
|
12 | 11 | uneq2i | |
13 | ssun2 | |
|
14 | ssequn1 | |
|
15 | 13 14 | mpbi | |
16 | 10 12 15 | 3eqtri | |
17 | 9 16 | uneq12i | |
18 | unidm | |
|
19 | 17 18 | eqtri | |
20 | 19 | reseq2i | |
21 | ssun2 | |
|
22 | 20 21 | eqsstri | |
23 | 1 | elexi | |
24 | dmexg | |
|
25 | rnexg | |
|
26 | 24 25 | unexd | |
27 | 26 | resiexd | |
28 | 1 27 | ax-mp | |
29 | 23 28 | unex | |
30 | dmeq | |
|
31 | rneq | |
|
32 | 30 31 | uneq12d | |
33 | 32 | reseq2d | |
34 | id | |
|
35 | 33 34 | sseq12d | |
36 | 35 | cleq2lem | |
37 | 29 36 | spcev | |
38 | intexab | |
|
39 | 37 38 | sylib | |
40 | 2 22 39 | mp2an | |