Metamath Proof Explorer

Theorem dfrcl2

Description: Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020)

Ref Expression
Assertion dfrcl2 r* = ( 𝑥 ∈ V ↦ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 df-rcl ⊢ r* = ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } )
2 rabab ⊢ { 𝑧 ∈ V ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } = { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) }
3 2 eqcomi ⊢ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } = { 𝑧 ∈ V ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) }
4 3 inteqi ⊢ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } = ∩ { 𝑧 ∈ V ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) }
5 4 a1i ⊢ ( 𝑥 ∈ V → ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } = ∩ { 𝑧 ∈ V ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } )
6 vex ⊢ 𝑥 ∈ V
7 6 dmex ⊢ dom 𝑥 ∈ V
8 6 rnex ⊢ ran 𝑥 ∈ V
9 7 8 unex ⊢ ( dom 𝑥 ∪ ran 𝑥 ) ∈ V
10 resiexg ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∈ V → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V )
11 9 10 ax-mp ⊢ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∈ V
12 11 6 unex ⊢ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∈ V
13 12 a1i ⊢ ( 𝑥 ∈ V → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∈ V )
14 ssun2 ⊢ 𝑥 ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 )
15 dmun ⊢ dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) = ( dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ dom 𝑥 )
16 dmresi ⊢ dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
17 16 uneq1i ⊢ ( dom ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ dom 𝑥 ) = ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ dom 𝑥 )
18 un23 ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ dom 𝑥 ) = ( ( dom 𝑥 ∪ dom 𝑥 ) ∪ ran 𝑥 )
19 unidm ⊢ ( dom 𝑥 ∪ dom 𝑥 ) = dom 𝑥
20 19 uneq1i ⊢ ( ( dom 𝑥 ∪ dom 𝑥 ) ∪ ran 𝑥 ) = ( dom 𝑥 ∪ ran 𝑥 )
21 18 20 eqtri ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ dom 𝑥 ) = ( dom 𝑥 ∪ ran 𝑥 )
22 15 17 21 3eqtri ⊢ dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) = ( dom 𝑥 ∪ ran 𝑥 )
23 rnun ⊢ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) = ( ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ ran 𝑥 )
24 rnresi ⊢ ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
25 24 uneq1i ⊢ ( ran ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ ran 𝑥 ) = ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ran 𝑥 )
26 unass ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ran 𝑥 ) = ( dom 𝑥 ∪ ( ran 𝑥 ∪ ran 𝑥 ) )
27 unidm ⊢ ( ran 𝑥 ∪ ran 𝑥 ) = ran 𝑥
28 27 uneq2i ⊢ ( dom 𝑥 ∪ ( ran 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
29 26 28 eqtri ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ran 𝑥 ) = ( dom 𝑥 ∪ ran 𝑥 )
30 23 25 29 3eqtri ⊢ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) = ( dom 𝑥 ∪ ran 𝑥 )
31 22 30 uneq12i ⊢ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) = ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ( dom 𝑥 ∪ ran 𝑥 ) )
32 unidm ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∪ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
33 31 32 eqtri ⊢ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) = ( dom 𝑥 ∪ ran 𝑥 )
34 33 reseq2i ⊢ ( I ↾ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) = ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) )
35 ssun1 ⊢ ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 )
36 34 35 eqsstri ⊢ ( I ↾ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 )
37 14 36 pm3.2i ⊢ ( 𝑥 ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∧ ( I ↾ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
38 dmeq ⊢ ( 𝑧 = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) → dom 𝑧 = dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
39 rneq ⊢ ( 𝑧 = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) → ran 𝑧 = ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
40 38 39 uneq12d ⊢ ( 𝑧 = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) → ( dom 𝑧 ∪ ran 𝑧 ) = ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) )
41 40 reseq2d ⊢ ( 𝑧 = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) → ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) = ( I ↾ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) )
42 id ⊢ ( 𝑧 = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) → 𝑧 = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
43 41 42 sseq12d ⊢ ( 𝑧 = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) → ( ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ↔ ( I ↾ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) )
44 43 cleq2lem ⊢ ( 𝑧 = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) → ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) ↔ ( 𝑥 ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∧ ( I ↾ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) )
45 44 intminss ⊢ ( ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∈ V ∧ ( 𝑥 ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∧ ( I ↾ ( dom ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ∪ ran ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ) ) → ∩ { 𝑧 ∈ V ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
46 13 37 45 sylancl ⊢ ( 𝑥 ∈ V → ∩ { 𝑧 ∈ V ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
47 5 46 eqsstrd ⊢ ( 𝑥 ∈ V → ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } ⊆ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
48 dmss ⊢ ( 𝑥 ⊆ 𝑧 → dom 𝑥 ⊆ dom 𝑧 )
49 rnss ⊢ ( 𝑥 ⊆ 𝑧 → ran 𝑥 ⊆ ran 𝑧 )
50 unss12 ⊢ ( ( dom 𝑥 ⊆ dom 𝑧 ∧ ran 𝑥 ⊆ ran 𝑧 ) → ( dom 𝑥 ∪ ran 𝑥 ) ⊆ ( dom 𝑧 ∪ ran 𝑧 ) )
51 48 49 50 syl2anc ⊢ ( 𝑥 ⊆ 𝑧 → ( dom 𝑥 ∪ ran 𝑥 ) ⊆ ( dom 𝑧 ∪ ran 𝑧 ) )
52 dfss ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ⊆ ( dom 𝑧 ∪ ran 𝑧 ) ↔ ( dom 𝑥 ∪ ran 𝑥 ) = ( ( dom 𝑥 ∪ ran 𝑥 ) ∩ ( dom 𝑧 ∪ ran 𝑧 ) ) )
53 51 52 sylib ⊢ ( 𝑥 ⊆ 𝑧 → ( dom 𝑥 ∪ ran 𝑥 ) = ( ( dom 𝑥 ∪ ran 𝑥 ) ∩ ( dom 𝑧 ∪ ran 𝑧 ) ) )
54 incom ⊢ ( ( dom 𝑥 ∪ ran 𝑥 ) ∩ ( dom 𝑧 ∪ ran 𝑧 ) ) = ( ( dom 𝑧 ∪ ran 𝑧 ) ∩ ( dom 𝑥 ∪ ran 𝑥 ) )
55 53 54 eqtrdi ⊢ ( 𝑥 ⊆ 𝑧 → ( dom 𝑥 ∪ ran 𝑥 ) = ( ( dom 𝑧 ∪ ran 𝑧 ) ∩ ( dom 𝑥 ∪ ran 𝑥 ) ) )
56 55 reseq2d ⊢ ( 𝑥 ⊆ 𝑧 → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( ( dom 𝑧 ∪ ran 𝑧 ) ∩ ( dom 𝑥 ∪ ran 𝑥 ) ) ) )
57 resres ⊢ ( ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( I ↾ ( ( dom 𝑧 ∪ ran 𝑧 ) ∩ ( dom 𝑥 ∪ ran 𝑥 ) ) )
58 56 57 eqtr4di ⊢ ( 𝑥 ⊆ 𝑧 → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) = ( ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) )
59 resss ⊢ ( ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) )
60 59 a1i ⊢ ( 𝑥 ⊆ 𝑧 → ( ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) )
61 58 60 eqsstrd ⊢ ( 𝑥 ⊆ 𝑧 → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) )
62 61 adantr ⊢ ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) )
63 simpr ⊢ ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) → ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 )
64 62 63 sstrd ⊢ ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) → ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ⊆ 𝑧 )
65 simpl ⊢ ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) → 𝑥 ⊆ 𝑧 )
66 64 65 unssd ⊢ ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ⊆ 𝑧 )
67 66 ax-gen ⊢ ∀ 𝑧 ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ⊆ 𝑧 )
68 67 a1i ⊢ ( 𝑥 ∈ V → ∀ 𝑧 ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ⊆ 𝑧 ) )
69 ssintab ⊢ ( ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ⊆ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } ↔ ∀ 𝑧 ( ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ⊆ 𝑧 ) )
70 68 69 sylibr ⊢ ( 𝑥 ∈ V → ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) ⊆ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } )
71 47 70 eqssd ⊢ ( 𝑥 ∈ V → ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } = ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
72 71 mpteq2ia ⊢ ( 𝑥 ∈ V ↦ ∩ { 𝑧 ∣ ( 𝑥 ⊆ 𝑧 ∧ ( I ↾ ( dom 𝑧 ∪ ran 𝑧 ) ) ⊆ 𝑧 ) } ) = ( 𝑥 ∈ V ↦ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )
73 1 72 eqtri ⊢ r* = ( 𝑥 ∈ V ↦ ( ( I ↾ ( dom 𝑥 ∪ ran 𝑥 ) ) ∪ 𝑥 ) )