Proof of Theorem comptiunov2i
| Step | Hyp | Ref
| Expression |
| 1 | | comptiunov2.x |
. . . 4
⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖)) |
| 2 | 1 | funmpt2 6605 |
. . 3
⊢ Fun 𝑋 |
| 3 | | comptiunov2.y |
. . . 4
⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗)) |
| 4 | 3 | funmpt2 6605 |
. . 3
⊢ Fun 𝑌 |
| 5 | | funco 6606 |
. . 3
⊢ ((Fun
𝑋 ∧ Fun 𝑌) → Fun (𝑋 ∘ 𝑌)) |
| 6 | 2, 4, 5 | mp2an 692 |
. 2
⊢ Fun
(𝑋 ∘ 𝑌) |
| 7 | | comptiunov2.z |
. . 3
⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘)) |
| 8 | 7 | funmpt2 6605 |
. 2
⊢ Fun 𝑍 |
| 9 | | ssv 4008 |
. . . . . . 7
⊢ ran 𝑌 ⊆ V |
| 10 | | comptiunov2.i |
. . . . . . . . 9
⊢ 𝐼 ∈ V |
| 11 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑎 ↑ 𝑖) ∈ V |
| 12 | 10, 11 | iunex 7993 |
. . . . . . . 8
⊢ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) ∈ V |
| 13 | 12, 1 | dmmpti 6712 |
. . . . . . 7
⊢ dom 𝑋 = V |
| 14 | 9, 13 | sseqtrri 4033 |
. . . . . 6
⊢ ran 𝑌 ⊆ dom 𝑋 |
| 15 | | dmcosseq 5987 |
. . . . . 6
⊢ (ran
𝑌 ⊆ dom 𝑋 → dom (𝑋 ∘ 𝑌) = dom 𝑌) |
| 16 | 14, 15 | ax-mp 5 |
. . . . 5
⊢ dom
(𝑋 ∘ 𝑌) = dom 𝑌 |
| 17 | | comptiunov2.j |
. . . . . . 7
⊢ 𝐽 ∈ V |
| 18 | | ovex 7464 |
. . . . . . 7
⊢ (𝑏 ↑ 𝑗) ∈ V |
| 19 | 17, 18 | iunex 7993 |
. . . . . 6
⊢ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) ∈ V |
| 20 | 19, 3 | dmmpti 6712 |
. . . . 5
⊢ dom 𝑌 = V |
| 21 | 16, 20 | eqtri 2765 |
. . . 4
⊢ dom
(𝑋 ∘ 𝑌) = V |
| 22 | | comptiunov2.k |
. . . . . . 7
⊢ 𝐾 = (𝐼 ∪ 𝐽) |
| 23 | 10, 17 | unex 7764 |
. . . . . . 7
⊢ (𝐼 ∪ 𝐽) ∈ V |
| 24 | 22, 23 | eqeltri 2837 |
. . . . . 6
⊢ 𝐾 ∈ V |
| 25 | | ovex 7464 |
. . . . . 6
⊢ (𝑐 ↑ 𝑘) ∈ V |
| 26 | 24, 25 | iunex 7993 |
. . . . 5
⊢ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) ∈ V |
| 27 | 26, 7 | dmmpti 6712 |
. . . 4
⊢ dom 𝑍 = V |
| 28 | 21, 27 | eqtr4i 2768 |
. . 3
⊢ dom
(𝑋 ∘ 𝑌) = dom 𝑍 |
| 29 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
| 30 | 29, 20 | eleqtrri 2840 |
. . . . . . . 8
⊢ 𝑑 ∈ dom 𝑌 |
| 31 | | fvco 7007 |
. . . . . . . 8
⊢ ((Fun
𝑌 ∧ 𝑑 ∈ dom 𝑌) → ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑))) |
| 32 | 4, 30, 31 | mp2an 692 |
. . . . . . 7
⊢ ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑)) |
| 33 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (𝑏 ↑ 𝑗) = (𝑑 ↑ 𝑗)) |
| 34 | 33 | iuneq2d 5022 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑑 → ∪
𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) |
| 35 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑑 ↑ 𝑗) ∈ V |
| 36 | 17, 35 | iunex 7993 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V |
| 37 | 34, 3, 36 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝑑 ∈ V → (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) |
| 38 | 37 | elv 3485 |
. . . . . . . 8
⊢ (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) |
| 39 | 38 | fveq2i 6909 |
. . . . . . 7
⊢ (𝑋‘(𝑌‘𝑑)) = (𝑋‘∪
𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) |
| 40 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → (𝑎 ↑ 𝑖) = (∪
𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)) |
| 41 | 40 | iuneq2d 5022 |
. . . . . . . . 9
⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → ∪
𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)) |
| 42 | | ovex 7464 |
. . . . . . . . . 10
⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V |
| 43 | 10, 42 | iunex 7993 |
. . . . . . . . 9
⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V |
| 44 | 41, 1, 43 | fvmpt 7016 |
. . . . . . . 8
⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V → (𝑋‘∪
𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)) |
| 45 | 36, 44 | ax-mp 5 |
. . . . . . 7
⊢ (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
| 46 | 32, 39, 45 | 3eqtri 2769 |
. . . . . 6
⊢ ((𝑋 ∘ 𝑌)‘𝑑) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
| 47 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑐 = 𝑑 → (𝑐 ↑ 𝑘) = (𝑑 ↑ 𝑘)) |
| 48 | 47 | iuneq2d 5022 |
. . . . . . . 8
⊢ (𝑐 = 𝑑 → ∪
𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
| 49 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑑 ↑ 𝑘) ∈ V |
| 50 | 24, 49 | iunex 7993 |
. . . . . . . 8
⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) ∈ V |
| 51 | 48, 7, 50 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑑 ∈ V → (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
| 52 | 51 | elv 3485 |
. . . . . 6
⊢ (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) |
| 53 | 46, 52 | eqeq12i 2755 |
. . . . 5
⊢ (((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
| 54 | 21, 53 | raleqbii 3344 |
. . . 4
⊢
(∀𝑑 ∈
dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∀𝑑 ∈ V ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
| 55 | | comptiunov2.3 |
. . . . . . 7
⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪
𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) |
| 56 | | iunxun 5094 |
. . . . . . . 8
⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) = (∪
𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪
𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘)) |
| 57 | | comptiunov2.1 |
. . . . . . . . 9
⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
| 58 | | comptiunov2.2 |
. . . . . . . . 9
⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
| 59 | 57, 58 | unssi 4191 |
. . . . . . . 8
⊢ (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪
𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘)) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
| 60 | 56, 59 | eqsstri 4030 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⊆ ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
| 61 | 55, 60 | eqssi 4000 |
. . . . . 6
⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) |
| 62 | | iuneq1 5008 |
. . . . . . 7
⊢ (𝐾 = (𝐼 ∪ 𝐽) → ∪
𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)) |
| 63 | 22, 62 | ax-mp 5 |
. . . . . 6
⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) |
| 64 | 61, 63 | eqtr4i 2768 |
. . . . 5
⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) |
| 65 | 64 | a1i 11 |
. . . 4
⊢ (𝑑 ∈ V → ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
| 66 | 54, 65 | mprgbir 3068 |
. . 3
⊢
∀𝑑 ∈ dom
(𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) |
| 67 | | eqfunfv 7056 |
. . . 4
⊢ ((Fun
(𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((𝑋 ∘ 𝑌) = 𝑍 ↔ (dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)))) |
| 68 | 67 | biimprd 248 |
. . 3
⊢ ((Fun
(𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)) → (𝑋 ∘ 𝑌) = 𝑍)) |
| 69 | 28, 66, 68 | mp2ani 698 |
. 2
⊢ ((Fun
(𝑋 ∘ 𝑌) ∧ Fun 𝑍) → (𝑋 ∘ 𝑌) = 𝑍) |
| 70 | 6, 8, 69 | mp2an 692 |
1
⊢ (𝑋 ∘ 𝑌) = 𝑍 |