Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dfrcl2 Structured version   Visualization version   GIF version

Theorem dfrcl2 42194
Description: Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020.)
Assertion
Ref Expression
dfrcl2 r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))

Proof of Theorem dfrcl2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-rcl 42193 . 2 r* = (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)})
2 rabab 3501 . . . . . . . 8 {𝑧 ∈ V ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}
32eqcomi 2740 . . . . . . 7 {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = {𝑧 ∈ V ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}
43inteqi 4947 . . . . . 6 {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = {𝑧 ∈ V ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}
54a1i 11 . . . . 5 (𝑥 ∈ V → {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = {𝑧 ∈ V ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)})
6 vex 3477 . . . . . . . . . . 11 𝑥 ∈ V
76dmex 7884 . . . . . . . . . 10 dom 𝑥 ∈ V
86rnex 7885 . . . . . . . . . 10 ran 𝑥 ∈ V
97, 8unex 7716 . . . . . . . . 9 (dom 𝑥 ∪ ran 𝑥) ∈ V
10 resiexg 7887 . . . . . . . . 9 ((dom 𝑥 ∪ ran 𝑥) ∈ V → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∈ V)
119, 10ax-mp 5 . . . . . . . 8 ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∈ V
1211, 6unex 7716 . . . . . . 7 (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∈ V
1312a1i 11 . . . . . 6 (𝑥 ∈ V → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∈ V)
14 ssun2 4169 . . . . . . 7 𝑥 ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)
15 dmun 5902 . . . . . . . . . . . 12 dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) = (dom ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ dom 𝑥)
16 dmresi 6041 . . . . . . . . . . . . 13 dom ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥)
1716uneq1i 4155 . . . . . . . . . . . 12 (dom ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ dom 𝑥) = ((dom 𝑥 ∪ ran 𝑥) ∪ dom 𝑥)
18 un23 4164 . . . . . . . . . . . . 13 ((dom 𝑥 ∪ ran 𝑥) ∪ dom 𝑥) = ((dom 𝑥 ∪ dom 𝑥) ∪ ran 𝑥)
19 unidm 4148 . . . . . . . . . . . . . 14 (dom 𝑥 ∪ dom 𝑥) = dom 𝑥
2019uneq1i 4155 . . . . . . . . . . . . 13 ((dom 𝑥 ∪ dom 𝑥) ∪ ran 𝑥) = (dom 𝑥 ∪ ran 𝑥)
2118, 20eqtri 2759 . . . . . . . . . . . 12 ((dom 𝑥 ∪ ran 𝑥) ∪ dom 𝑥) = (dom 𝑥 ∪ ran 𝑥)
2215, 17, 213eqtri 2763 . . . . . . . . . . 11 dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) = (dom 𝑥 ∪ ran 𝑥)
23 rnun 6134 . . . . . . . . . . . 12 ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) = (ran ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ ran 𝑥)
24 rnresi 6063 . . . . . . . . . . . . 13 ran ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥)
2524uneq1i 4155 . . . . . . . . . . . 12 (ran ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ ran 𝑥) = ((dom 𝑥 ∪ ran 𝑥) ∪ ran 𝑥)
26 unass 4162 . . . . . . . . . . . . 13 ((dom 𝑥 ∪ ran 𝑥) ∪ ran 𝑥) = (dom 𝑥 ∪ (ran 𝑥 ∪ ran 𝑥))
27 unidm 4148 . . . . . . . . . . . . . 14 (ran 𝑥 ∪ ran 𝑥) = ran 𝑥
2827uneq2i 4156 . . . . . . . . . . . . 13 (dom 𝑥 ∪ (ran 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥)
2926, 28eqtri 2759 . . . . . . . . . . . 12 ((dom 𝑥 ∪ ran 𝑥) ∪ ran 𝑥) = (dom 𝑥 ∪ ran 𝑥)
3023, 25, 293eqtri 2763 . . . . . . . . . . 11 ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) = (dom 𝑥 ∪ ran 𝑥)
3122, 30uneq12i 4157 . . . . . . . . . 10 (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) = ((dom 𝑥 ∪ ran 𝑥) ∪ (dom 𝑥 ∪ ran 𝑥))
32 unidm 4148 . . . . . . . . . 10 ((dom 𝑥 ∪ ran 𝑥) ∪ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥)
3331, 32eqtri 2759 . . . . . . . . 9 (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) = (dom 𝑥 ∪ ran 𝑥)
3433reseq2i 5970 . . . . . . . 8 ( I ↾ (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) = ( I ↾ (dom 𝑥 ∪ ran 𝑥))
35 ssun1 4168 . . . . . . . 8 ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)
3634, 35eqsstri 4012 . . . . . . 7 ( I ↾ (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)
3714, 36pm3.2i 471 . . . . . 6 (𝑥 ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∧ ( I ↾ (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
38 dmeq 5895 . . . . . . . . . . 11 (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → dom 𝑧 = dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
39 rneq 5927 . . . . . . . . . . 11 (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → ran 𝑧 = ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
4038, 39uneq12d 4160 . . . . . . . . . 10 (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → (dom 𝑧 ∪ ran 𝑧) = (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)))
4140reseq2d 5973 . . . . . . . . 9 (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → ( I ↾ (dom 𝑧 ∪ ran 𝑧)) = ( I ↾ (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))))
42 id 22 . . . . . . . . 9 (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → 𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
4341, 42sseq12d 4011 . . . . . . . 8 (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → (( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧 ↔ ( I ↾ (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)))
4443cleq2lem 42128 . . . . . . 7 (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → ((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) ↔ (𝑥 ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∧ ( I ↾ (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))))
4544intminss 4971 . . . . . 6 (((( 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 𝑥)) ∪ 𝑥))
4613, 37, 45sylancl 586 . . . . 5 (𝑥 ∈ V → {𝑧 ∈ V ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
475, 46eqsstrd 4016 . . . 4 (𝑥 ∈ V → {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
48 dmss 5894 . . . . . . . . . . . . . . . 16 (𝑥𝑧 → dom 𝑥 ⊆ dom 𝑧)
49 rnss 5930 . . . . . . . . . . . . . . . 16 (𝑥𝑧 → ran 𝑥 ⊆ ran 𝑧)
50 unss12 4178 . . . . . . . . . . . . . . . 16 ((dom 𝑥 ⊆ dom 𝑧 ∧ ran 𝑥 ⊆ ran 𝑧) → (dom 𝑥 ∪ ran 𝑥) ⊆ (dom 𝑧 ∪ ran 𝑧))
5148, 49, 50syl2anc 584 . . . . . . . . . . . . . . 15 (𝑥𝑧 → (dom 𝑥 ∪ ran 𝑥) ⊆ (dom 𝑧 ∪ ran 𝑧))
52 dfss 3962 . . . . . . . . . . . . . . 15 ((dom 𝑥 ∪ ran 𝑥) ⊆ (dom 𝑧 ∪ ran 𝑧) ↔ (dom 𝑥 ∪ ran 𝑥) = ((dom 𝑥 ∪ ran 𝑥) ∩ (dom 𝑧 ∪ ran 𝑧)))
5351, 52sylib 217 . . . . . . . . . . . . . 14 (𝑥𝑧 → (dom 𝑥 ∪ ran 𝑥) = ((dom 𝑥 ∪ ran 𝑥) ∩ (dom 𝑧 ∪ ran 𝑧)))
54 incom 4197 . . . . . . . . . . . . . 14 ((dom 𝑥 ∪ ran 𝑥) ∩ (dom 𝑧 ∪ ran 𝑧)) = ((dom 𝑧 ∪ ran 𝑧) ∩ (dom 𝑥 ∪ ran 𝑥))
5553, 54eqtrdi 2787 . . . . . . . . . . . . 13 (𝑥𝑧 → (dom 𝑥 ∪ ran 𝑥) = ((dom 𝑧 ∪ ran 𝑧) ∩ (dom 𝑥 ∪ ran 𝑥)))
5655reseq2d 5973 . . . . . . . . . . . 12 (𝑥𝑧 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ ((dom 𝑧 ∪ ran 𝑧) ∩ (dom 𝑥 ∪ ran 𝑥))))
57 resres 5986 . . . . . . . . . . . 12 (( I ↾ (dom 𝑧 ∪ ran 𝑧)) ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ ((dom 𝑧 ∪ ran 𝑧) ∩ (dom 𝑥 ∪ ran 𝑥)))
5856, 57eqtr4di 2789 . . . . . . . . . . 11 (𝑥𝑧 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = (( I ↾ (dom 𝑧 ∪ ran 𝑧)) ↾ (dom 𝑥 ∪ ran 𝑥)))
59 resss 5998 . . . . . . . . . . . 12 (( I ↾ (dom 𝑧 ∪ ran 𝑧)) ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ( I ↾ (dom 𝑧 ∪ ran 𝑧))
6059a1i 11 . . . . . . . . . . 11 (𝑥𝑧 → (( I ↾ (dom 𝑧 ∪ ran 𝑧)) ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ( I ↾ (dom 𝑧 ∪ ran 𝑧)))
6158, 60eqsstrd 4016 . . . . . . . . . 10 (𝑥𝑧 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ( I ↾ (dom 𝑧 ∪ ran 𝑧)))
6261adantr 481 . . . . . . . . 9 ((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ( I ↾ (dom 𝑧 ∪ ran 𝑧)))
63 simpr 485 . . . . . . . . 9 ((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)
6462, 63sstrd 3988 . . . . . . . 8 ((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧)
65 simpl 483 . . . . . . . 8 ((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → 𝑥𝑧)
6664, 65unssd 4182 . . . . . . 7 ((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ 𝑧)
6766ax-gen 1797 . . . . . 6 𝑧((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ 𝑧)
6867a1i 11 . . . . 5 (𝑥 ∈ V → ∀𝑧((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ 𝑧))
69 ssintab 4962 . . . . 5 ((( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} ↔ ∀𝑧((𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ 𝑧))
7068, 69sylibr 233 . . . 4 (𝑥 ∈ V → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)})
7147, 70eqssd 3995 . . 3 (𝑥 ∈ V → {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
7271mpteq2ia 5244 . 2 (𝑥 ∈ V ↦ {𝑧 ∣ (𝑥𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}) = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
731, 72eqtri 2759 1 r* = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1539   = wceq 1541  wcel 2106  {cab 2708  {crab 3431  Vcvv 3473  cun 3942  cin 3943  wss 3944   cint 4943  cmpt 5224   I cid 5566  dom cdm 5669  ran crn 5670  cres 5671  r*crcl 42192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-int 4944  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-rcl 42193
This theorem is referenced by:  dfrcl3  42195
  Copyright terms: Public domain W3C validator