Step | Hyp | Ref
| Expression |
1 | | df-rtrcl 14882 |
. 2
⊢ t* =
(𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
2 | | ancom 462 |
. . . . . . 7
⊢ ((( I
↾ (dom 𝑦 ∪ ran
𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦) ↔ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)) |
3 | 2 | anbi2i 624 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦)) ↔ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))) |
4 | 3 | abbii 2803 |
. . . . 5
⊢ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))} = {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} |
5 | 4 | inteqi 4915 |
. . . 4
⊢ ∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))} = ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} |
6 | 5 | mpteq2i 5214 |
. . 3
⊢ (𝑥 ∈ V ↦ ∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))}) = (𝑥 ∈ V ↦ ∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) |
7 | | vex 3451 |
. . . . . 6
⊢ 𝑥 ∈ V |
8 | 7 | rtrclexi 41985 |
. . . . 5
⊢ ∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∈ V |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝑥 ∈ V → ∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∈ V) |
10 | | dmexg 7844 |
. . . . . . . . 9
⊢ (𝑥 ∈ V → dom 𝑥 ∈ V) |
11 | | rnexg 7845 |
. . . . . . . . 9
⊢ (𝑥 ∈ V → ran 𝑥 ∈ V) |
12 | 10, 11 | unexd 7692 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (dom 𝑥 ∪ ran 𝑥) ∈ V) |
13 | | resiexg 7855 |
. . . . . . . 8
⊢ ((dom
𝑥 ∪ ran 𝑥) ∈ V → ( I ↾
(dom 𝑥 ∪ ran 𝑥)) ∈ V) |
14 | 7, 12, 13 | mp2b 10 |
. . . . . . 7
⊢ ( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∈
V |
15 | 7, 14 | unex 7684 |
. . . . . 6
⊢ (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ∈ V |
16 | 15 | trclexi 41984 |
. . . . 5
⊢ ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∈ V |
17 | 16 | a1i 11 |
. . . 4
⊢ (𝑥 ∈ V → ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∈ V) |
18 | | simpr 486 |
. . . . . 6
⊢ (((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) → (𝑧 ∘ 𝑧) ⊆ 𝑧) |
19 | 18 | cotrintab 41978 |
. . . . 5
⊢ (∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∘ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) ⊆ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} |
20 | 19 | a1i 11 |
. . . 4
⊢ (𝑥 ∈ V → (∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∘ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) ⊆ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
21 | 7 | dmex 7852 |
. . . . . . . . . . . . 13
⊢ dom 𝑥 ∈ V |
22 | 7 | rnex 7853 |
. . . . . . . . . . . . 13
⊢ ran 𝑥 ∈ V |
23 | | unexg 7687 |
. . . . . . . . . . . . . 14
⊢ ((dom
𝑥 ∈ V ∧ ran 𝑥 ∈ V) → (dom 𝑥 ∪ ran 𝑥) ∈ V) |
24 | 23 | resiexd 7170 |
. . . . . . . . . . . . 13
⊢ ((dom
𝑥 ∈ V ∧ ran 𝑥 ∈ V) → ( I ↾
(dom 𝑥 ∪ ran 𝑥)) ∈ V) |
25 | 21, 22, 24 | mp2an 691 |
. . . . . . . . . . . 12
⊢ ( I
↾ (dom 𝑥 ∪ ran
𝑥)) ∈
V |
26 | 7, 25 | unex 7684 |
. . . . . . . . . . 11
⊢ (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ∈ V |
27 | | dmtrcl 41991 |
. . . . . . . . . . 11
⊢ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ∈ V → dom ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = dom (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥)))) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . 10
⊢ dom ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = dom (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) |
29 | | dmun 5870 |
. . . . . . . . . . 11
⊢ dom
(𝑥 ∪ ( I ↾ (dom
𝑥 ∪ ran 𝑥))) = (dom 𝑥 ∪ dom ( I ↾ (dom 𝑥 ∪ ran 𝑥))) |
30 | | dmresi 6009 |
. . . . . . . . . . . 12
⊢ dom ( I
↾ (dom 𝑥 ∪ ran
𝑥)) = (dom 𝑥 ∪ ran 𝑥) |
31 | 30 | uneq2i 4124 |
. . . . . . . . . . 11
⊢ (dom
𝑥 ∪ dom ( I ↾
(dom 𝑥 ∪ ran 𝑥))) = (dom 𝑥 ∪ (dom 𝑥 ∪ ran 𝑥)) |
32 | | ssun1 4136 |
. . . . . . . . . . . 12
⊢ dom 𝑥 ⊆ (dom 𝑥 ∪ ran 𝑥) |
33 | | ssequn1 4144 |
. . . . . . . . . . . 12
⊢ (dom
𝑥 ⊆ (dom 𝑥 ∪ ran 𝑥) ↔ (dom 𝑥 ∪ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥)) |
34 | 32, 33 | mpbi 229 |
. . . . . . . . . . 11
⊢ (dom
𝑥 ∪ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥) |
35 | 29, 31, 34 | 3eqtri 2765 |
. . . . . . . . . 10
⊢ dom
(𝑥 ∪ ( I ↾ (dom
𝑥 ∪ ran 𝑥))) = (dom 𝑥 ∪ ran 𝑥) |
36 | 28, 35 | eqtri 2761 |
. . . . . . . . 9
⊢ dom ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = (dom 𝑥 ∪ ran 𝑥) |
37 | | rntrcl 41992 |
. . . . . . . . . . 11
⊢ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ∈ V → ran ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = ran (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥)))) |
38 | 26, 37 | ax-mp 5 |
. . . . . . . . . 10
⊢ ran ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = ran (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) |
39 | | rnun 6102 |
. . . . . . . . . . 11
⊢ ran
(𝑥 ∪ ( I ↾ (dom
𝑥 ∪ ran 𝑥))) = (ran 𝑥 ∪ ran ( I ↾ (dom 𝑥 ∪ ran 𝑥))) |
40 | | rnresi 6031 |
. . . . . . . . . . . 12
⊢ ran ( I
↾ (dom 𝑥 ∪ ran
𝑥)) = (dom 𝑥 ∪ ran 𝑥) |
41 | 40 | uneq2i 4124 |
. . . . . . . . . . 11
⊢ (ran
𝑥 ∪ ran ( I ↾
(dom 𝑥 ∪ ran 𝑥))) = (ran 𝑥 ∪ (dom 𝑥 ∪ ran 𝑥)) |
42 | | ssun2 4137 |
. . . . . . . . . . . 12
⊢ ran 𝑥 ⊆ (dom 𝑥 ∪ ran 𝑥) |
43 | | ssequn1 4144 |
. . . . . . . . . . . 12
⊢ (ran
𝑥 ⊆ (dom 𝑥 ∪ ran 𝑥) ↔ (ran 𝑥 ∪ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥)) |
44 | 42, 43 | mpbi 229 |
. . . . . . . . . . 11
⊢ (ran
𝑥 ∪ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥) |
45 | 39, 41, 44 | 3eqtri 2765 |
. . . . . . . . . 10
⊢ ran
(𝑥 ∪ ( I ↾ (dom
𝑥 ∪ ran 𝑥))) = (dom 𝑥 ∪ ran 𝑥) |
46 | 38, 45 | eqtri 2761 |
. . . . . . . . 9
⊢ ran ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = (dom 𝑥 ∪ ran 𝑥) |
47 | 36, 46 | uneq12i 4125 |
. . . . . . . 8
⊢ (dom
∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∪ ran ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) = ((dom 𝑥 ∪ ran 𝑥) ∪ (dom 𝑥 ∪ ran 𝑥)) |
48 | | unidm 4116 |
. . . . . . . 8
⊢ ((dom
𝑥 ∪ ran 𝑥) ∪ (dom 𝑥 ∪ ran 𝑥)) = (dom 𝑥 ∪ ran 𝑥) |
49 | 47, 48 | eqtri 2761 |
. . . . . . 7
⊢ (dom
∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∪ ran ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) = (dom 𝑥 ∪ ran 𝑥) |
50 | 49 | reseq2i 5938 |
. . . . . 6
⊢ ( I
↾ (dom ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∪ ran ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) = ( I ↾ (dom 𝑥 ∪ ran 𝑥)) |
51 | | ssun2 4137 |
. . . . . . 7
⊢ ( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) |
52 | | ssmin 4932 |
. . . . . . 7
⊢ (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} |
53 | 51, 52 | sstri 3957 |
. . . . . 6
⊢ ( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} |
54 | 50, 53 | eqsstri 3982 |
. . . . 5
⊢ ( I
↾ (dom ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∪ ran ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) ⊆ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} |
55 | 54 | a1i 11 |
. . . 4
⊢ (𝑥 ∈ V → ( I ↾
(dom ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∪ ran ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) ⊆ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
56 | | simprl 770 |
. . . . . 6
⊢ ((𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)) → (𝑦 ∘ 𝑦) ⊆ 𝑦) |
57 | 56 | cotrintab 41978 |
. . . . 5
⊢ (∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∘ ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) ⊆ ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} |
58 | 57 | a1i 11 |
. . . 4
⊢ (𝑥 ∈ V → (∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∘ ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) ⊆ ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) |
59 | | id 22 |
. . . . . 6
⊢ (𝑦 = ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → 𝑦 = ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
60 | 59, 59 | coeq12d 5824 |
. . . . 5
⊢ (𝑦 = ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → (𝑦 ∘ 𝑦) = (∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∘ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) |
61 | 60, 59 | sseq12d 3981 |
. . . 4
⊢ (𝑦 = ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → ((𝑦 ∘ 𝑦) ⊆ 𝑦 ↔ (∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∘ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) ⊆ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) |
62 | | dmeq 5863 |
. . . . . . 7
⊢ (𝑦 = ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → dom 𝑦 = dom ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
63 | | rneq 5895 |
. . . . . . 7
⊢ (𝑦 = ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → ran 𝑦 = ran ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
64 | 62, 63 | uneq12d 4128 |
. . . . . 6
⊢ (𝑦 = ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → (dom 𝑦 ∪ ran 𝑦) = (dom ∩ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∪ ran ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) |
65 | 64 | reseq2d 5941 |
. . . . 5
⊢ (𝑦 = ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → ( I ↾ (dom 𝑦 ∪ ran 𝑦)) = ( I ↾ (dom ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∪ ran ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}))) |
66 | 65, 59 | sseq12d 3981 |
. . . 4
⊢ (𝑦 = ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ↔ ( I ↾ (dom ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ∪ ran ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) ⊆ ∩
{𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)})) |
67 | | id 22 |
. . . . . 6
⊢ (𝑧 = ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} → 𝑧 = ∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) |
68 | 67, 67 | coeq12d 5824 |
. . . . 5
⊢ (𝑧 = ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} → (𝑧 ∘ 𝑧) = (∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∘ ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))})) |
69 | 68, 67 | sseq12d 3981 |
. . . 4
⊢ (𝑧 = ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} → ((𝑧 ∘ 𝑧) ⊆ 𝑧 ↔ (∩ {𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))} ∘ ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) ⊆ ∩
{𝑦 ∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))})) |
70 | 9, 17, 20, 55, 58, 61, 66, 69 | mptrcllem 41977 |
. . 3
⊢ (𝑥 ∈ V ↦ ∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ ((𝑦 ∘ 𝑦) ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦))}) = (𝑥 ∈ V ↦ ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
71 | | df-3an 1090 |
. . . . . . 7
⊢ ((( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ ((( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧) ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)) |
72 | | ancom 462 |
. . . . . . . . 9
⊢ ((( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧) ↔ (𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧)) |
73 | | unss 4148 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ 𝑧 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧) ↔ (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧) |
74 | 72, 73 | bitri 275 |
. . . . . . . 8
⊢ ((( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧) ↔ (𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧) |
75 | 74 | anbi1i 625 |
. . . . . . 7
⊢ (((( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧) ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)) |
76 | 71, 75 | bitr2i 276 |
. . . . . 6
⊢ (((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)) |
77 | 76 | abbii 2803 |
. . . . 5
⊢ {𝑧 ∣ ((𝑥 ∪ ( I ↾ (dom 𝑥 ∪ ran 𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = {𝑧 ∣ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} |
78 | 77 | inteqi 4915 |
. . . 4
⊢ ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = ∩ {𝑧 ∣ (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} |
79 | 78 | mpteq2i 5214 |
. . 3
⊢ (𝑥 ∈ V ↦ ∩ {𝑧
∣ ((𝑥 ∪ ( I
↾ (dom 𝑥 ∪ ran
𝑥))) ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) = (𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
80 | 6, 70, 79 | 3eqtri 2765 |
. 2
⊢ (𝑥 ∈ V ↦ ∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))}) = (𝑥 ∈ V ↦ ∩ {𝑧
∣ (( I ↾ (dom 𝑥
∪ ran 𝑥)) ⊆ 𝑧 ∧ 𝑥 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
81 | 1, 80 | eqtr4i 2764 |
1
⊢ t* =
(𝑥 ∈ V ↦ ∩ {𝑦
∣ (𝑥 ⊆ 𝑦 ∧ (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ∧ (𝑦 ∘ 𝑦) ⊆ 𝑦))}) |