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* = x ∈ V ⟼ I ↾ dom ⁡ x ∪ ran ⁡ x ∪ x

Proof

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