Proof of Theorem cnvrcl0
Step | Hyp | Ref
| Expression |
1 | | cnvresid 5882 |
. . . . . . 7
⊢ ◡( I ↾ (dom 𝑦 ∪ ran 𝑦)) = ( I ↾ (dom 𝑦 ∪ ran 𝑦)) |
2 | | cnvnonrel 36913 |
. . . . . . . . . . . . . . . 16
⊢ ◡(𝑋 ∖ ◡◡𝑋) = ∅ |
3 | | cnv0 5454 |
. . . . . . . . . . . . . . . 16
⊢ ◡∅ = ∅ |
4 | 2, 3 | eqtr4i 2635 |
. . . . . . . . . . . . . . 15
⊢ ◡(𝑋 ∖ ◡◡𝑋) = ◡∅ |
5 | 4 | dmeqi 5247 |
. . . . . . . . . . . . . 14
⊢ dom ◡(𝑋 ∖ ◡◡𝑋) = dom ◡∅ |
6 | | df-rn 5049 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑋 ∖ ◡◡𝑋) = dom ◡(𝑋 ∖ ◡◡𝑋) |
7 | | df-rn 5049 |
. . . . . . . . . . . . . 14
⊢ ran
∅ = dom ◡∅ |
8 | 5, 6, 7 | 3eqtr4i 2642 |
. . . . . . . . . . . . 13
⊢ ran
(𝑋 ∖ ◡◡𝑋) = ran ∅ |
9 | | 0ss 3924 |
. . . . . . . . . . . . . 14
⊢ ∅
⊆ ◡𝑦 |
10 | | rnss 5275 |
. . . . . . . . . . . . . 14
⊢ (∅
⊆ ◡𝑦 → ran ∅ ⊆ ran ◡𝑦) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ ran
∅ ⊆ ran ◡𝑦 |
12 | 8, 11 | eqsstri 3598 |
. . . . . . . . . . . 12
⊢ ran
(𝑋 ∖ ◡◡𝑋) ⊆ ran ◡𝑦 |
13 | | ssequn2 3748 |
. . . . . . . . . . . 12
⊢ (ran
(𝑋 ∖ ◡◡𝑋) ⊆ ran ◡𝑦 ↔ (ran ◡𝑦 ∪ ran (𝑋 ∖ ◡◡𝑋)) = ran ◡𝑦) |
14 | 12, 13 | mpbi 219 |
. . . . . . . . . . 11
⊢ (ran
◡𝑦 ∪ ran (𝑋 ∖ ◡◡𝑋)) = ran ◡𝑦 |
15 | | rnun 5460 |
. . . . . . . . . . 11
⊢ ran
(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (ran ◡𝑦 ∪ ran (𝑋 ∖ ◡◡𝑋)) |
16 | | dfdm4 5238 |
. . . . . . . . . . 11
⊢ dom 𝑦 = ran ◡𝑦 |
17 | 14, 15, 16 | 3eqtr4ri 2643 |
. . . . . . . . . 10
⊢ dom 𝑦 = ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) |
18 | 4 | rneqi 5273 |
. . . . . . . . . . . . . 14
⊢ ran ◡(𝑋 ∖ ◡◡𝑋) = ran ◡∅ |
19 | | dfdm4 5238 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑋 ∖ ◡◡𝑋) = ran ◡(𝑋 ∖ ◡◡𝑋) |
20 | | dfdm4 5238 |
. . . . . . . . . . . . . 14
⊢ dom
∅ = ran ◡∅ |
21 | 18, 19, 20 | 3eqtr4i 2642 |
. . . . . . . . . . . . 13
⊢ dom
(𝑋 ∖ ◡◡𝑋) = dom ∅ |
22 | | dmss 5245 |
. . . . . . . . . . . . . 14
⊢ (∅
⊆ ◡𝑦 → dom ∅ ⊆ dom ◡𝑦) |
23 | 9, 22 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ dom
∅ ⊆ dom ◡𝑦 |
24 | 21, 23 | eqsstri 3598 |
. . . . . . . . . . . 12
⊢ dom
(𝑋 ∖ ◡◡𝑋) ⊆ dom ◡𝑦 |
25 | | ssequn2 3748 |
. . . . . . . . . . . 12
⊢ (dom
(𝑋 ∖ ◡◡𝑋) ⊆ dom ◡𝑦 ↔ (dom ◡𝑦 ∪ dom (𝑋 ∖ ◡◡𝑋)) = dom ◡𝑦) |
26 | 24, 25 | mpbi 219 |
. . . . . . . . . . 11
⊢ (dom
◡𝑦 ∪ dom (𝑋 ∖ ◡◡𝑋)) = dom ◡𝑦 |
27 | | dmun 5253 |
. . . . . . . . . . 11
⊢ dom
(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (dom ◡𝑦 ∪ dom (𝑋 ∖ ◡◡𝑋)) |
28 | | df-rn 5049 |
. . . . . . . . . . 11
⊢ ran 𝑦 = dom ◡𝑦 |
29 | 26, 27, 28 | 3eqtr4ri 2643 |
. . . . . . . . . 10
⊢ ran 𝑦 = dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) |
30 | 17, 29 | uneq12i 3727 |
. . . . . . . . 9
⊢ (dom
𝑦 ∪ ran 𝑦) = (ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
31 | 30 | equncomi 3721 |
. . . . . . . 8
⊢ (dom
𝑦 ∪ ran 𝑦) = (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
32 | 31 | reseq2i 5314 |
. . . . . . 7
⊢ ( I
↾ (dom 𝑦 ∪ ran
𝑦)) = ( I ↾ (dom
(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) |
33 | 1, 32 | eqtr2i 2633 |
. . . . . 6
⊢ ( I
↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) = ◡( I ↾ (dom 𝑦 ∪ ran 𝑦)) |
34 | | cnvss 5216 |
. . . . . 6
⊢ (( I
↾ (dom 𝑦 ∪ ran
𝑦)) ⊆ 𝑦 → ◡( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ ◡𝑦) |
35 | 33, 34 | syl5eqss 3612 |
. . . . 5
⊢ (( I
↾ (dom 𝑦 ∪ ran
𝑦)) ⊆ 𝑦 → ( I ↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) ⊆ ◡𝑦) |
36 | | ssun1 3738 |
. . . . 5
⊢ ◡𝑦 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) |
37 | 35, 36 | syl6ss 3580 |
. . . 4
⊢ (( I
↾ (dom 𝑦 ∪ ran
𝑦)) ⊆ 𝑦 → ( I ↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
38 | | dmeq 5246 |
. . . . . . 7
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → dom 𝑥 = dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
39 | | rneq 5272 |
. . . . . . 7
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ran 𝑥 = ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
40 | 38, 39 | uneq12d 3730 |
. . . . . 6
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (dom 𝑥 ∪ ran 𝑥) = (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) |
41 | 40 | reseq2d 5317 |
. . . . 5
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))) |
42 | | id 22 |
. . . . 5
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) |
43 | 41, 42 | sseq12d 3597 |
. . . 4
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 ↔ ( I ↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) |
44 | 37, 43 | syl5ibr 235 |
. . 3
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) |
45 | 44 | adantl 481 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) |
46 | | cnvresid 5882 |
. . . . . 6
⊢ ◡( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom 𝑥 ∪ ran 𝑥)) |
47 | | dfdm4 5238 |
. . . . . . . . 9
⊢ dom 𝑥 = ran ◡𝑥 |
48 | | df-rn 5049 |
. . . . . . . . 9
⊢ ran 𝑥 = dom ◡𝑥 |
49 | 47, 48 | uneq12i 3727 |
. . . . . . . 8
⊢ (dom
𝑥 ∪ ran 𝑥) = (ran ◡𝑥 ∪ dom ◡𝑥) |
50 | 49 | equncomi 3721 |
. . . . . . 7
⊢ (dom
𝑥 ∪ ran 𝑥) = (dom ◡𝑥 ∪ ran ◡𝑥) |
51 | 50 | reseq2i 5314 |
. . . . . 6
⊢ ( I
↾ (dom 𝑥 ∪ ran
𝑥)) = ( I ↾ (dom
◡𝑥 ∪ ran ◡𝑥)) |
52 | 46, 51 | eqtr2i 2633 |
. . . . 5
⊢ ( I
↾ (dom ◡𝑥 ∪ ran ◡𝑥)) = ◡( I ↾ (dom 𝑥 ∪ ran 𝑥)) |
53 | | cnvss 5216 |
. . . . 5
⊢ (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ 𝑥 → ◡( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ◡𝑥) |
54 | 52, 53 | syl5eqss 3612 |
. . . 4
⊢ (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ 𝑥 → ( I ↾ (dom ◡𝑥 ∪ ran ◡𝑥)) ⊆ ◡𝑥) |
55 | | dmeq 5246 |
. . . . . . 7
⊢ (𝑦 = ◡𝑥 → dom 𝑦 = dom ◡𝑥) |
56 | | rneq 5272 |
. . . . . . 7
⊢ (𝑦 = ◡𝑥 → ran 𝑦 = ran ◡𝑥) |
57 | 55, 56 | uneq12d 3730 |
. . . . . 6
⊢ (𝑦 = ◡𝑥 → (dom 𝑦 ∪ ran 𝑦) = (dom ◡𝑥 ∪ ran ◡𝑥)) |
58 | 57 | reseq2d 5317 |
. . . . 5
⊢ (𝑦 = ◡𝑥 → ( I ↾ (dom 𝑦 ∪ ran 𝑦)) = ( I ↾ (dom ◡𝑥 ∪ ran ◡𝑥))) |
59 | | id 22 |
. . . . 5
⊢ (𝑦 = ◡𝑥 → 𝑦 = ◡𝑥) |
60 | 58, 59 | sseq12d 3597 |
. . . 4
⊢ (𝑦 = ◡𝑥 → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ↔ ( I ↾ (dom ◡𝑥 ∪ ran ◡𝑥)) ⊆ ◡𝑥)) |
61 | 54, 60 | syl5ibr 235 |
. . 3
⊢ (𝑦 = ◡𝑥 → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 → ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)) |
62 | 61 | adantl 481 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ◡𝑥) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 → ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)) |
63 | | dmeq 5246 |
. . . . 5
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → dom 𝑥 = dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) |
64 | | rneq 5272 |
. . . . 5
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → ran 𝑥 = ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) |
65 | 63, 64 | uneq12d 3730 |
. . . 4
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → (dom 𝑥 ∪ ran 𝑥) = (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) |
66 | 65 | reseq2d 5317 |
. . 3
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))))) |
67 | | id 22 |
. . 3
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → 𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) |
68 | 66, 67 | sseq12d 3597 |
. 2
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 ↔ ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) |
69 | | ssun1 3738 |
. . 3
⊢ 𝑋 ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) |
70 | 69 | a1i 11 |
. 2
⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) |
71 | | dmexg 6989 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → dom 𝑋 ∈ V) |
72 | | rnexg 6990 |
. . . . 5
⊢ (𝑋 ∈ 𝑉 → ran 𝑋 ∈ V) |
73 | | unexg 6857 |
. . . . 5
⊢ ((dom
𝑋 ∈ V ∧ ran 𝑋 ∈ V) → (dom 𝑋 ∪ ran 𝑋) ∈ V) |
74 | 71, 72, 73 | syl2anc 691 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → (dom 𝑋 ∪ ran 𝑋) ∈ V) |
75 | 74 | resiexd 6385 |
. . 3
⊢ (𝑋 ∈ 𝑉 → ( I ↾ (dom 𝑋 ∪ ran 𝑋)) ∈ V) |
76 | | unexg 6857 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ( I ↾ (dom 𝑋 ∪ ran 𝑋)) ∈ V) → (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∈ V) |
77 | 75, 76 | mpdan 699 |
. 2
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∈ V) |
78 | | dmun 5253 |
. . . . . 6
⊢ dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) = (dom 𝑋 ∪ dom ( I ↾ (dom 𝑋 ∪ ran 𝑋))) |
79 | | ssun1 3738 |
. . . . . . 7
⊢ dom 𝑋 ⊆ (dom 𝑋 ∪ ran 𝑋) |
80 | | dmresi 5376 |
. . . . . . . 8
⊢ dom ( I
↾ (dom 𝑋 ∪ ran
𝑋)) = (dom 𝑋 ∪ ran 𝑋) |
81 | 80 | eqimssi 3622 |
. . . . . . 7
⊢ dom ( I
↾ (dom 𝑋 ∪ ran
𝑋)) ⊆ (dom 𝑋 ∪ ran 𝑋) |
82 | 79, 81 | unssi 3750 |
. . . . . 6
⊢ (dom
𝑋 ∪ dom ( I ↾
(dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) |
83 | 78, 82 | eqsstri 3598 |
. . . . 5
⊢ dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) |
84 | | rnun 5460 |
. . . . . 6
⊢ ran
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) = (ran 𝑋 ∪ ran ( I ↾ (dom 𝑋 ∪ ran 𝑋))) |
85 | | ssun2 3739 |
. . . . . . 7
⊢ ran 𝑋 ⊆ (dom 𝑋 ∪ ran 𝑋) |
86 | | rnresi 5398 |
. . . . . . . 8
⊢ ran ( I
↾ (dom 𝑋 ∪ ran
𝑋)) = (dom 𝑋 ∪ ran 𝑋) |
87 | 86 | eqimssi 3622 |
. . . . . . 7
⊢ ran ( I
↾ (dom 𝑋 ∪ ran
𝑋)) ⊆ (dom 𝑋 ∪ ran 𝑋) |
88 | 85, 87 | unssi 3750 |
. . . . . 6
⊢ (ran
𝑋 ∪ ran ( I ↾
(dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) |
89 | 84, 88 | eqsstri 3598 |
. . . . 5
⊢ ran
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) |
90 | 83, 89 | pm3.2i 470 |
. . . 4
⊢ (dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) ∧ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋)) |
91 | | unss 3749 |
. . . . 5
⊢ ((dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) ∧ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋)) ↔ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) ⊆ (dom 𝑋 ∪ ran 𝑋)) |
92 | | ssres2 5345 |
. . . . 5
⊢ ((dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) ⊆ (dom 𝑋 ∪ ran 𝑋) → ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) |
93 | 91, 92 | sylbi 206 |
. . . 4
⊢ ((dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) ∧ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋)) → ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) |
94 | | ssun4 3741 |
. . . 4
⊢ (( I
↾ (dom (𝑋 ∪ ( I
↾ (dom 𝑋 ∪ ran
𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ ( I ↾ (dom 𝑋 ∪ ran 𝑋)) → ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) |
95 | 90, 93, 94 | mp2b 10 |
. . 3
⊢ ( I
↾ (dom (𝑋 ∪ ( I
↾ (dom 𝑋 ∪ ran
𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) |
96 | 95 | a1i 11 |
. 2
⊢ (𝑋 ∈ 𝑉 → ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) |
97 | 45, 62, 68, 70, 77, 96 | clcnvlem 36949 |
1
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)}) |