Proof of Theorem cnvrcl0
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cnvresid 6645 | . . . . . . 7
⊢ ◡( I ↾ (dom 𝑦 ∪ ran 𝑦)) = ( I ↾ (dom 𝑦 ∪ ran 𝑦)) | 
| 2 |  | cnvnonrel 43601 | . . . . . . . . . . . . . . . 16
⊢ ◡(𝑋 ∖ ◡◡𝑋) = ∅ | 
| 3 |  | cnv0 6160 | . . . . . . . . . . . . . . . 16
⊢ ◡∅ = ∅ | 
| 4 | 2, 3 | eqtr4i 2768 | . . . . . . . . . . . . . . 15
⊢ ◡(𝑋 ∖ ◡◡𝑋) = ◡∅ | 
| 5 | 4 | dmeqi 5915 | . . . . . . . . . . . . . 14
⊢ dom ◡(𝑋 ∖ ◡◡𝑋) = dom ◡∅ | 
| 6 |  | df-rn 5696 | . . . . . . . . . . . . . 14
⊢ ran
(𝑋 ∖ ◡◡𝑋) = dom ◡(𝑋 ∖ ◡◡𝑋) | 
| 7 |  | df-rn 5696 | . . . . . . . . . . . . . 14
⊢ ran
∅ = dom ◡∅ | 
| 8 | 5, 6, 7 | 3eqtr4i 2775 | . . . . . . . . . . . . 13
⊢ ran
(𝑋 ∖ ◡◡𝑋) = ran ∅ | 
| 9 |  | 0ss 4400 | . . . . . . . . . . . . . 14
⊢ ∅
⊆ ◡𝑦 | 
| 10 | 9 | rnssi 5951 | . . . . . . . . . . . . 13
⊢ ran
∅ ⊆ ran ◡𝑦 | 
| 11 | 8, 10 | eqsstri 4030 | . . . . . . . . . . . 12
⊢ ran
(𝑋 ∖ ◡◡𝑋) ⊆ ran ◡𝑦 | 
| 12 |  | ssequn2 4189 | . . . . . . . . . . . 12
⊢ (ran
(𝑋 ∖ ◡◡𝑋) ⊆ ran ◡𝑦 ↔ (ran ◡𝑦 ∪ ran (𝑋 ∖ ◡◡𝑋)) = ran ◡𝑦) | 
| 13 | 11, 12 | mpbi 230 | . . . . . . . . . . 11
⊢ (ran
◡𝑦 ∪ ran (𝑋 ∖ ◡◡𝑋)) = ran ◡𝑦 | 
| 14 |  | rnun 6165 | . . . . . . . . . . 11
⊢ ran
(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (ran ◡𝑦 ∪ ran (𝑋 ∖ ◡◡𝑋)) | 
| 15 |  | dfdm4 5906 | . . . . . . . . . . 11
⊢ dom 𝑦 = ran ◡𝑦 | 
| 16 | 13, 14, 15 | 3eqtr4ri 2776 | . . . . . . . . . 10
⊢ dom 𝑦 = ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) | 
| 17 | 4 | rneqi 5948 | . . . . . . . . . . . . . 14
⊢ ran ◡(𝑋 ∖ ◡◡𝑋) = ran ◡∅ | 
| 18 |  | dfdm4 5906 | . . . . . . . . . . . . . 14
⊢ dom
(𝑋 ∖ ◡◡𝑋) = ran ◡(𝑋 ∖ ◡◡𝑋) | 
| 19 |  | dfdm4 5906 | . . . . . . . . . . . . . 14
⊢ dom
∅ = ran ◡∅ | 
| 20 | 17, 18, 19 | 3eqtr4i 2775 | . . . . . . . . . . . . 13
⊢ dom
(𝑋 ∖ ◡◡𝑋) = dom ∅ | 
| 21 |  | dmss 5913 | . . . . . . . . . . . . . 14
⊢ (∅
⊆ ◡𝑦 → dom ∅ ⊆ dom ◡𝑦) | 
| 22 | 9, 21 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ dom
∅ ⊆ dom ◡𝑦 | 
| 23 | 20, 22 | eqsstri 4030 | . . . . . . . . . . . 12
⊢ dom
(𝑋 ∖ ◡◡𝑋) ⊆ dom ◡𝑦 | 
| 24 |  | ssequn2 4189 | . . . . . . . . . . . 12
⊢ (dom
(𝑋 ∖ ◡◡𝑋) ⊆ dom ◡𝑦 ↔ (dom ◡𝑦 ∪ dom (𝑋 ∖ ◡◡𝑋)) = dom ◡𝑦) | 
| 25 | 23, 24 | mpbi 230 | . . . . . . . . . . 11
⊢ (dom
◡𝑦 ∪ dom (𝑋 ∖ ◡◡𝑋)) = dom ◡𝑦 | 
| 26 |  | dmun 5921 | . . . . . . . . . . 11
⊢ dom
(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) = (dom ◡𝑦 ∪ dom (𝑋 ∖ ◡◡𝑋)) | 
| 27 |  | df-rn 5696 | . . . . . . . . . . 11
⊢ ran 𝑦 = dom ◡𝑦 | 
| 28 | 25, 26, 27 | 3eqtr4ri 2776 | . . . . . . . . . 10
⊢ ran 𝑦 = dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) | 
| 29 | 16, 28 | uneq12i 4166 | . . . . . . . . 9
⊢ (dom
𝑦 ∪ ran 𝑦) = (ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) | 
| 30 | 29 | equncomi 4160 | . . . . . . . 8
⊢ (dom
𝑦 ∪ ran 𝑦) = (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) | 
| 31 | 30 | reseq2i 5994 | . . . . . . 7
⊢ ( I
↾ (dom 𝑦 ∪ ran
𝑦)) = ( I ↾ (dom
(◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) | 
| 32 | 1, 31 | eqtr2i 2766 | . . . . . 6
⊢ ( I
↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) = ◡( I ↾ (dom 𝑦 ∪ ran 𝑦)) | 
| 33 |  | cnvss 5883 | . . . . . 6
⊢ (( I
↾ (dom 𝑦 ∪ ran
𝑦)) ⊆ 𝑦 → ◡( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ ◡𝑦) | 
| 34 | 32, 33 | eqsstrid 4022 | . . . . 5
⊢ (( I
↾ (dom 𝑦 ∪ ran
𝑦)) ⊆ 𝑦 → ( I ↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) ⊆ ◡𝑦) | 
| 35 |  | ssun1 4178 | . . . . 5
⊢ ◡𝑦 ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) | 
| 36 | 34, 35 | sstrdi 3996 | . . . 4
⊢ (( I
↾ (dom 𝑦 ∪ ran
𝑦)) ⊆ 𝑦 → ( I ↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) | 
| 37 |  | dmeq 5914 | . . . . . . 7
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → dom 𝑥 = dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) | 
| 38 |  | rneq 5947 | . . . . . . 7
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ran 𝑥 = ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) | 
| 39 | 37, 38 | uneq12d 4169 | . . . . . 6
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (dom 𝑥 ∪ ran 𝑥) = (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) | 
| 40 | 39 | reseq2d 5997 | . . . . 5
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))))) | 
| 41 |  | id 22 | . . . . 5
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) | 
| 42 | 40, 41 | sseq12d 4017 | . . . 4
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 ↔ ( I ↾ (dom (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) ∪ ran (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) ⊆ (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)))) | 
| 43 | 36, 42 | imbitrrid 246 | . . 3
⊢ (𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋)) → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) | 
| 44 | 43 | adantl 481 | . 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑥 = (◡𝑦 ∪ (𝑋 ∖ ◡◡𝑋))) → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)) | 
| 45 |  | cnvresid 6645 | . . . . . 6
⊢ ◡( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom 𝑥 ∪ ran 𝑥)) | 
| 46 |  | dfdm4 5906 | . . . . . . . . 9
⊢ dom 𝑥 = ran ◡𝑥 | 
| 47 |  | df-rn 5696 | . . . . . . . . 9
⊢ ran 𝑥 = dom ◡𝑥 | 
| 48 | 46, 47 | uneq12i 4166 | . . . . . . . 8
⊢ (dom
𝑥 ∪ ran 𝑥) = (ran ◡𝑥 ∪ dom ◡𝑥) | 
| 49 | 48 | equncomi 4160 | . . . . . . 7
⊢ (dom
𝑥 ∪ ran 𝑥) = (dom ◡𝑥 ∪ ran ◡𝑥) | 
| 50 | 49 | reseq2i 5994 | . . . . . 6
⊢ ( I
↾ (dom 𝑥 ∪ ran
𝑥)) = ( I ↾ (dom
◡𝑥 ∪ ran ◡𝑥)) | 
| 51 | 45, 50 | eqtr2i 2766 | . . . . 5
⊢ ( I
↾ (dom ◡𝑥 ∪ ran ◡𝑥)) = ◡( I ↾ (dom 𝑥 ∪ ran 𝑥)) | 
| 52 |  | cnvss 5883 | . . . . 5
⊢ (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ 𝑥 → ◡( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ ◡𝑥) | 
| 53 | 51, 52 | eqsstrid 4022 | . . . 4
⊢ (( I
↾ (dom 𝑥 ∪ ran
𝑥)) ⊆ 𝑥 → ( I ↾ (dom ◡𝑥 ∪ ran ◡𝑥)) ⊆ ◡𝑥) | 
| 54 |  | dmeq 5914 | . . . . . . 7
⊢ (𝑦 = ◡𝑥 → dom 𝑦 = dom ◡𝑥) | 
| 55 |  | rneq 5947 | . . . . . . 7
⊢ (𝑦 = ◡𝑥 → ran 𝑦 = ran ◡𝑥) | 
| 56 | 54, 55 | uneq12d 4169 | . . . . . 6
⊢ (𝑦 = ◡𝑥 → (dom 𝑦 ∪ ran 𝑦) = (dom ◡𝑥 ∪ ran ◡𝑥)) | 
| 57 | 56 | reseq2d 5997 | . . . . 5
⊢ (𝑦 = ◡𝑥 → ( I ↾ (dom 𝑦 ∪ ran 𝑦)) = ( I ↾ (dom ◡𝑥 ∪ ran ◡𝑥))) | 
| 58 |  | id 22 | . . . . 5
⊢ (𝑦 = ◡𝑥 → 𝑦 = ◡𝑥) | 
| 59 | 57, 58 | sseq12d 4017 | . . . 4
⊢ (𝑦 = ◡𝑥 → (( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦 ↔ ( I ↾ (dom ◡𝑥 ∪ ran ◡𝑥)) ⊆ ◡𝑥)) | 
| 60 | 53, 59 | imbitrrid 246 | . . 3
⊢ (𝑦 = ◡𝑥 → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 → ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)) | 
| 61 | 60 | adantl 481 | . 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 = ◡𝑥) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 → ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)) | 
| 62 |  | dmeq 5914 | . . . . 5
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → dom 𝑥 = dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) | 
| 63 |  | rneq 5947 | . . . . 5
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → ran 𝑥 = ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) | 
| 64 | 62, 63 | uneq12d 4169 | . . . 4
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → (dom 𝑥 ∪ ran 𝑥) = (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) | 
| 65 | 64 | reseq2d 5997 | . . 3
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → ( I ↾ (dom 𝑥 ∪ ran 𝑥)) = ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))))) | 
| 66 |  | id 22 | . . 3
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → 𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) | 
| 67 | 65, 66 | sseq12d 4017 | . 2
⊢ (𝑥 = (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) → (( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥 ↔ ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) | 
| 68 |  | ssun1 4178 | . . 3
⊢ 𝑋 ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) | 
| 69 | 68 | a1i 11 | . 2
⊢ (𝑋 ∈ 𝑉 → 𝑋 ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) | 
| 70 |  | dmexg 7923 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → dom 𝑋 ∈ V) | 
| 71 |  | rnexg 7924 | . . . . 5
⊢ (𝑋 ∈ 𝑉 → ran 𝑋 ∈ V) | 
| 72 | 70, 71 | unexd 7774 | . . . 4
⊢ (𝑋 ∈ 𝑉 → (dom 𝑋 ∪ ran 𝑋) ∈ V) | 
| 73 | 72 | resiexd 7236 | . . 3
⊢ (𝑋 ∈ 𝑉 → ( I ↾ (dom 𝑋 ∪ ran 𝑋)) ∈ V) | 
| 74 |  | unexg 7763 | . . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ( I ↾ (dom 𝑋 ∪ ran 𝑋)) ∈ V) → (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∈ V) | 
| 75 | 73, 74 | mpdan 687 | . 2
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∈ V) | 
| 76 |  | dmun 5921 | . . . . . 6
⊢ dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) = (dom 𝑋 ∪ dom ( I ↾ (dom 𝑋 ∪ ran 𝑋))) | 
| 77 |  | ssun1 4178 | . . . . . . 7
⊢ dom 𝑋 ⊆ (dom 𝑋 ∪ ran 𝑋) | 
| 78 |  | resdmss 6255 | . . . . . . 7
⊢ dom ( I
↾ (dom 𝑋 ∪ ran
𝑋)) ⊆ (dom 𝑋 ∪ ran 𝑋) | 
| 79 | 77, 78 | unssi 4191 | . . . . . 6
⊢ (dom
𝑋 ∪ dom ( I ↾
(dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) | 
| 80 | 76, 79 | eqsstri 4030 | . . . . 5
⊢ dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) | 
| 81 |  | rnun 6165 | . . . . . 6
⊢ ran
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) = (ran 𝑋 ∪ ran ( I ↾ (dom 𝑋 ∪ ran 𝑋))) | 
| 82 |  | ssun2 4179 | . . . . . . 7
⊢ ran 𝑋 ⊆ (dom 𝑋 ∪ ran 𝑋) | 
| 83 |  | rnresi 6093 | . . . . . . . 8
⊢ ran ( I
↾ (dom 𝑋 ∪ ran
𝑋)) = (dom 𝑋 ∪ ran 𝑋) | 
| 84 | 83 | eqimssi 4044 | . . . . . . 7
⊢ ran ( I
↾ (dom 𝑋 ∪ ran
𝑋)) ⊆ (dom 𝑋 ∪ ran 𝑋) | 
| 85 | 82, 84 | unssi 4191 | . . . . . 6
⊢ (ran
𝑋 ∪ ran ( I ↾
(dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) | 
| 86 | 81, 85 | eqsstri 4030 | . . . . 5
⊢ ran
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) | 
| 87 | 80, 86 | pm3.2i 470 | . . . 4
⊢ (dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) ∧ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋)) | 
| 88 |  | unss 4190 | . . . . 5
⊢ ((dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋) ∧ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ⊆ (dom 𝑋 ∪ ran 𝑋)) ↔ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) ⊆ (dom 𝑋 ∪ ran 𝑋)) | 
| 89 |  | ssres2 6022 | . . . . 5
⊢ ((dom
(𝑋 ∪ ( I ↾ (dom
𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) ⊆ (dom 𝑋 ∪ ran 𝑋) → ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) | 
| 90 | 88, 89 | sylbi 217 | . . . 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 𝑋))) | 
| 91 |  | ssun4 4181 | . . . 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 𝑋)))) | 
| 92 | 87, 90, 91 | mp2b 10 | . . 3
⊢ ( I
↾ (dom (𝑋 ∪ ( I
↾ (dom 𝑋 ∪ ran
𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) | 
| 93 | 92 | a1i 11 | . 2
⊢ (𝑋 ∈ 𝑉 → ( I ↾ (dom (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))) ∪ ran (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋))))) ⊆ (𝑋 ∪ ( I ↾ (dom 𝑋 ∪ ran 𝑋)))) | 
| 94 | 44, 61, 67, 69, 75, 93 | clcnvlem 43636 | 1
⊢ (𝑋 ∈ 𝑉 → ◡∩ {𝑥 ∣ (𝑋 ⊆ 𝑥 ∧ ( I ↾ (dom 𝑥 ∪ ran 𝑥)) ⊆ 𝑥)} = ∩ {𝑦 ∣ (◡𝑋 ⊆ 𝑦 ∧ ( I ↾ (dom 𝑦 ∪ ran 𝑦)) ⊆ 𝑦)}) |