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 24 25 unexd ⊢ ( 𝐴 ∈ 𝑉 → ( dom 𝐴 ∪ ran 𝐴 ) ∈ V )
27 26 resiexd ⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ∈ V )
28 1 27 ax-mp ⊢ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ∈ V
29 23 28 unex ⊢ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∈ V
30 dmeq ⊢ ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → dom 𝑥 = dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
31 rneq ⊢ ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ran 𝑥 = ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
32 30 31 uneq12d ⊢ ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( dom 𝑥 ∪ ran 𝑥 ) = ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
33 32 reseq2d ⊢ ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) )
34 id ⊢ ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) )
35 33 34 sseq12d ⊢ ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ↔ ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) )
36 35 cleq2lem ⊢ ( 𝑥 = ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) → ( ( 𝐴 ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ↔ ( 𝐴 ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) )
37 29 36 spcev ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) )
38 intexab ⊢ ( ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) ↔ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } ∈ V )
39 37 38 sylib ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∧ ( I ↾ ( dom ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ∪ ran ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) ) ⊆ ( 𝐴 ∪ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ) ) → ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } ∈ V )
40 2 22 39 mp2an ⊢ ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑥 ) } ∈ V