Metamath Proof Explorer


Theorem rclexi

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

Ref Expression
Hypothesis rclexi.1 𝐴𝑉
Assertion rclexi { 𝑥 ∣ ( 𝐴𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } ∈ V

Proof

Step Hyp Ref Expression
1 rclexi.1 𝐴𝑉
2 ssun1 𝐴 ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
3 dmun dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ dom ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
4 dmresi dom ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
5 4 uneq2i ( dom 𝐴 ∪ dom ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) )
6 ssun1 dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
7 ssequn1 ( dom 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ↔ ( dom 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 ) )
8 6 7 mpbi ( dom 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
9 3 5 8 3eqtri dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ ran 𝐴 )
10 rnun ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( ran 𝐴 ∪ ran ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
11 rnresi ran ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
12 11 uneq2i ( ran 𝐴 ∪ ran ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( ran 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) )
13 ssun2 ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 )
14 ssequn1 ( ran 𝐴 ⊆ ( dom 𝐴 ∪ ran 𝐴 ) ↔ ( ran 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 ) )
15 13 14 mpbi ( ran 𝐴 ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
16 10 12 15 3eqtri ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) = ( dom 𝐴 ∪ ran 𝐴 )
17 9 16 uneq12i ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( ( dom 𝐴 ∪ ran 𝐴 ) ∪ ( dom 𝐴 ∪ ran 𝐴 ) )
18 unidm ( ( dom 𝐴 ∪ ran 𝐴 ) ∪ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( dom 𝐴 ∪ ran 𝐴 )
19 17 18 eqtri ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) = ( dom 𝐴 ∪ ran 𝐴 )
20 19 reseq2i ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) = ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) )
21 ssun2 ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
22 20 21 eqsstri ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) )
23 1 elexi 𝐴 ∈ V
24 dmexg ( 𝐴𝑉 → dom 𝐴 ∈ V )
25 rnexg ( 𝐴𝑉 → ran 𝐴 ∈ V )
26 unexg ( ( dom 𝐴 ∈ V ∧ ran 𝐴 ∈ V ) → ( dom 𝐴 ∪ ran 𝐴 ) ∈ V )
27 24 25 26 syl2anc ( 𝐴𝑉 → ( dom 𝐴 ∪ ran 𝐴 ) ∈ V )
28 27 resiexd ( 𝐴𝑉 → ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ∈ V )
29 1 28 ax-mp ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ∈ V
30 23 29 unex ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∈ V
31 dmeq ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → dom 𝑥 = dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
32 rneq ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ran 𝑥 = ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
33 31 32 uneq12d ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( dom 𝑥 ∪ ran 𝑥 ) = ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
34 33 reseq2d ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) )
35 id ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
36 34 35 sseq12d ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ↔ ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
37 36 cleq2lem ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( ( 𝐴𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ↔ ( 𝐴 ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) )
38 30 37 spcev ( ( 𝐴 ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) → ∃ 𝑥 ( 𝐴𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) )
39 intexab ( ∃ 𝑥 ( 𝐴𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ↔ { 𝑥 ∣ ( 𝐴𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } ∈ V )
40 38 39 sylib ( ( 𝐴 ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) → { 𝑥 ∣ ( 𝐴𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } ∈ V )
41 2 22 40 mp2an { 𝑥 ∣ ( 𝐴𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } ∈ V