| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-rcl 43691 | . 2
⊢ r* =
(𝑥 ∈ V ↦ ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}) | 
| 2 |  | rabab 3511 | . . . . . . . 8
⊢ {𝑧 ∈ V ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} | 
| 3 | 2 | eqcomi 2745 | . . . . . . 7
⊢ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = {𝑧 ∈ V ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} | 
| 4 | 3 | inteqi 4949 | . . . . . 6
⊢ ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = ∩ {𝑧 ∈ V ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} | 
| 5 | 4 | a1i 11 | . . . . 5
⊢ (𝑥 ∈ V → ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = ∩ {𝑧 ∈ V ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}) | 
| 6 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑥 ∈ V | 
| 7 | 6 | dmex 7932 | . . . . . . . . . 10
⊢ dom 𝑥 ∈ V | 
| 8 | 6 | rnex 7933 | . . . . . . . . . 10
⊢ ran 𝑥 ∈ V | 
| 9 | 7, 8 | unex 7765 | . . . . . . . . 9
⊢ (dom
𝑥 ∪ ran 𝑥) ∈ V | 
| 10 |  | resiexg 7935 | . . . . . . . . 9
⊢ ((dom
𝑥 ∪ ran 𝑥) ∈ V → ( I ↾
(dom 𝑥 ∪ ran 𝑥)) ∈ V) | 
| 11 | 9, 10 | ax-mp 5 | . . . . . . . 8
⊢ ( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∈
V | 
| 12 | 11, 6 | unex 7765 | . . . . . . 7
⊢ (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥) ∈ V | 
| 13 | 12 | a1i 11 | . . . . . 6
⊢ (𝑥 ∈ V → (( I ↾
(dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∈ V) | 
| 14 |  | ssun2 4178 | . . . . . . 7
⊢ 𝑥 ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) | 
| 15 |  | dmun 5920 | . . . . . . . . . . . 12
⊢ dom (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥) = (dom ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ dom 𝑥) | 
| 16 |  | dmresi 6069 | . . . . . . . . . . . . 13
⊢ dom ( I
↾ (dom 𝑥 ∪ ran
𝑥)) = (dom 𝑥 ∪ ran 𝑥) | 
| 17 | 16 | uneq1i 4163 | . . . . . . . . . . . 12
⊢ (dom ( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ dom 𝑥) = ((dom 𝑥 ∪ ran 𝑥) ∪ dom 𝑥) | 
| 18 |  | un23 4173 | . . . . . . . . . . . . 13
⊢ ((dom
𝑥 ∪ ran 𝑥) ∪ dom 𝑥) = ((dom 𝑥 ∪ dom 𝑥) ∪ ran 𝑥) | 
| 19 |  | unidm 4156 | . . . . . . . . . . . . . 14
⊢ (dom
𝑥 ∪ dom 𝑥) = dom 𝑥 | 
| 20 | 19 | uneq1i 4163 | . . . . . . . . . . . . 13
⊢ ((dom
𝑥 ∪ dom 𝑥) ∪ ran 𝑥) = (dom 𝑥 ∪ ran 𝑥) | 
| 21 | 18, 20 | eqtri 2764 | . . . . . . . . . . . 12
⊢ ((dom
𝑥 ∪ ran 𝑥) ∪ dom 𝑥) = (dom 𝑥 ∪ ran 𝑥) | 
| 22 | 15, 17, 21 | 3eqtri 2768 | . . . . . . . . . . 11
⊢ dom (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥) = (dom 𝑥 ∪ ran 𝑥) | 
| 23 |  | rnun 6164 | . . . . . . . . . . . 12
⊢ ran (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥) = (ran ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ ran 𝑥) | 
| 24 |  | rnresi 6092 | . . . . . . . . . . . . 13
⊢ ran ( I
↾ (dom 𝑥 ∪ ran
𝑥)) = (dom 𝑥 ∪ ran 𝑥) | 
| 25 | 24 | uneq1i 4163 | . . . . . . . . . . . 12
⊢ (ran ( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ ran 𝑥) = ((dom 𝑥 ∪ ran 𝑥) ∪ ran 𝑥) | 
| 26 |  | unass 4171 | . . . . . . . . . . . . 13
⊢ ((dom
𝑥 ∪ ran 𝑥) ∪ ran 𝑥) = (dom 𝑥 ∪ (ran 𝑥 ∪ ran 𝑥)) | 
| 27 |  | unidm 4156 | . . . . . . . . . . . . . 14
⊢ (ran
𝑥 ∪ ran 𝑥) = ran 𝑥 | 
| 28 | 27 | uneq2i 4164 | . . . . . . . . . . . . 13
⊢ (dom
𝑥 ∪ (ran 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥) | 
| 29 | 26, 28 | eqtri 2764 | . . . . . . . . . . . 12
⊢ ((dom
𝑥 ∪ ran 𝑥) ∪ ran 𝑥) = (dom 𝑥 ∪ ran 𝑥) | 
| 30 | 23, 25, 29 | 3eqtri 2768 | . . . . . . . . . . 11
⊢ ran (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥) = (dom 𝑥 ∪ ran 𝑥) | 
| 31 | 22, 30 | uneq12i 4165 | . . . . . . . . . 10
⊢ (dom (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom
𝑥 ∪ ran 𝑥)) ∪ 𝑥)) = ((dom 𝑥 ∪ ran 𝑥) ∪ (dom 𝑥 ∪ ran 𝑥)) | 
| 32 |  | unidm 4156 | . . . . . . . . . 10
⊢ ((dom
𝑥 ∪ ran 𝑥) ∪ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥) | 
| 33 | 31, 32 | eqtri 2764 | . . . . . . . . 9
⊢ (dom (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom
𝑥 ∪ ran 𝑥)) ∪ 𝑥)) = (dom 𝑥 ∪ ran 𝑥) | 
| 34 | 33 | reseq2i 5993 | . . . . . . . 8
⊢ ( I
↾ (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) = ( I ↾ (dom 𝑥 ∪ ran 𝑥)) | 
| 35 |  | ssun1 4177 | . . . . . . . 8
⊢ ( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ (( I ↾
(dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) | 
| 36 | 34, 35 | eqsstri 4029 | . . . . . . 7
⊢ ( I
↾ (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) | 
| 37 | 14, 36 | pm3.2i 470 | . . . . . 6
⊢ (𝑥 ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∧ ( I ↾ (dom (( I ↾ (dom
𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | 
| 38 |  | dmeq 5913 | . . . . . . . . . . 11
⊢ (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → dom 𝑧 = dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | 
| 39 |  | rneq 5946 | . . . . . . . . . . 11
⊢ (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → ran 𝑧 = ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | 
| 40 | 38, 39 | uneq12d 4168 | . . . . . . . . . 10
⊢ (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → (dom 𝑧 ∪ ran 𝑧) = (dom (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) | 
| 41 | 40 | reseq2d 5996 | . . . . . . . . 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 𝑥)) ∪ 𝑥)) | 
| 43 | 41, 42 | sseq12d 4016 | . . . . . . . 8
⊢ (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → (( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧 ↔ ( I ↾ (dom (( I ↾ (dom
𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) | 
| 44 | 43 | cleq2lem 43626 | . . . . . . 7
⊢ (𝑧 = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) → ((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) ↔ (𝑥 ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∧ ( I ↾ (dom (( I ↾ (dom
𝑥 ∪ ran 𝑥)) ∪ 𝑥) ∪ ran (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥))) ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)))) | 
| 45 | 44 | intminss 4973 | . . . . . 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 𝑥)) ∪ 𝑥)) | 
| 46 | 13, 37, 45 | sylancl 586 | . . . . 5
⊢ (𝑥 ∈ V → ∩ {𝑧
∈ V ∣ (𝑥 ⊆
𝑧 ∧ ( I ↾ (dom
𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | 
| 47 | 5, 46 | eqsstrd 4017 | . . . 4
⊢ (𝑥 ∈ V → ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} ⊆ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | 
| 48 |  | dmss 5912 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ⊆ 𝑧 → dom 𝑥 ⊆ dom 𝑧) | 
| 49 |  | rnss 5949 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ⊆ 𝑧 → ran 𝑥 ⊆ ran 𝑧) | 
| 50 |  | unss12 4187 | . . . . . . . . . . . . . . . 16
⊢ ((dom
𝑥 ⊆ dom 𝑧 ∧ ran 𝑥 ⊆ ran 𝑧) → (dom 𝑥 ∪ ran 𝑥) ⊆ (dom 𝑧 ∪ ran 𝑧)) | 
| 51 | 48, 49, 50 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ⊆ 𝑧 → (dom 𝑥 ∪ ran 𝑥) ⊆ (dom 𝑧 ∪ ran 𝑧)) | 
| 52 |  | dfss 3969 | . . . . . . . . . . . . . . 15
⊢ ((dom
𝑥 ∪ ran 𝑥) ⊆ (dom 𝑧 ∪ ran 𝑧) ↔ (dom 𝑥 ∪ ran 𝑥) = ((dom 𝑥 ∪ ran 𝑥) ∩ (dom 𝑧 ∪ ran 𝑧))) | 
| 53 | 51, 52 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ 𝑧 → (dom 𝑥 ∪ ran 𝑥) = ((dom 𝑥 ∪ ran 𝑥) ∩ (dom 𝑧 ∪ ran 𝑧))) | 
| 54 |  | incom 4208 | . . . . . . . . . . . . . 14
⊢ ((dom
𝑥 ∪ ran 𝑥) ∩ (dom 𝑧 ∪ ran 𝑧)) = ((dom 𝑧 ∪ ran 𝑧) ∩ (dom 𝑥 ∪ ran 𝑥)) | 
| 55 | 53, 54 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑥 ⊆ 𝑧 → (dom 𝑥 ∪ ran 𝑥) = ((dom 𝑧 ∪ ran 𝑧) ∩ (dom 𝑥 ∪ ran 𝑥))) | 
| 56 | 55 | reseq2d 5996 | . . . . . . . . . . . 12
⊢ (𝑥 ⊆ 𝑧 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ ((dom 𝑧 ∪ ran 𝑧) ∩ (dom 𝑥 ∪ ran 𝑥)))) | 
| 57 |  | resres 6009 | . . . . . . . . . . . 12
⊢ (( I
↾ (dom 𝑧 ∪ ran
𝑧)) ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ ((dom 𝑧 ∪ ran 𝑧) ∩ (dom 𝑥 ∪ ran 𝑥))) | 
| 58 | 56, 57 | eqtr4di 2794 | . . . . . . . . . . 11
⊢ (𝑥 ⊆ 𝑧 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = (( I ↾ (dom 𝑧 ∪ ran 𝑧)) ↾ (dom 𝑥 ∪ ran 𝑥))) | 
| 59 |  | resss 6018 | . . . . . . . . . . . 12
⊢ (( I
↾ (dom 𝑧 ∪ ran
𝑧)) ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) | 
| 60 | 59 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑥 ⊆ 𝑧 → (( I ↾ (dom 𝑧 ∪ ran 𝑧)) ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ( I ↾ (dom 𝑧 ∪ ran 𝑧))) | 
| 61 | 58, 60 | eqsstrd 4017 | . . . . . . . . . 10
⊢ (𝑥 ⊆ 𝑧 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ( I ↾ (dom 𝑧 ∪ ran 𝑧))) | 
| 62 | 61 | adantr 480 | . . . . . . . . 9
⊢ ((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ( I ↾ (dom 𝑧 ∪ ran 𝑧))) | 
| 63 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) | 
| 64 | 62, 63 | sstrd 3993 | . . . . . . . 8
⊢ ((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧) | 
| 65 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → 𝑥 ⊆ 𝑧) | 
| 66 | 64, 65 | unssd 4191 | . . . . . . 7
⊢ ((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ 𝑧) | 
| 67 | 66 | ax-gen 1794 | . . . . . 6
⊢
∀𝑧((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ 𝑧) | 
| 68 | 67 | a1i 11 | . . . . 5
⊢ (𝑥 ∈ V → ∀𝑧((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ 𝑧)) | 
| 69 |  | ssintab 4964 | . . . . 5
⊢ ((( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥) ⊆ ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} ↔ ∀𝑧((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ 𝑧)) | 
| 70 | 68, 69 | sylibr 234 | . . . 4
⊢ (𝑥 ∈ V → (( I ↾
(dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥) ⊆ ∩ {𝑧 ∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}) | 
| 71 | 47, 70 | eqssd 4000 | . . 3
⊢ (𝑥 ∈ V → ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)} = (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | 
| 72 | 71 | mpteq2ia 5244 | . 2
⊢ (𝑥 ∈ V ↦ ∩ {𝑧
∣ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑧 ∪ ran 𝑧)) ⊆ 𝑧)}) = (𝑥 ∈ V ↦ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ∪ 𝑥)) | 
| 73 | 1, 72 | eqtri 2764 | 1
⊢ r* =
(𝑥 ∈ V ↦ (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∪ 𝑥)) |