Proof of Theorem comptiunov2i
Step | Hyp | Ref
| Expression |
1 | | comptiunov2.x |
. . . 4
⊢ 𝑋 = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖)) |
2 | 1 | funmpt2 6372 |
. . 3
⊢ Fun 𝑋 |
3 | | comptiunov2.y |
. . . 4
⊢ 𝑌 = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗)) |
4 | 3 | funmpt2 6372 |
. . 3
⊢ Fun 𝑌 |
5 | | funco 6373 |
. . 3
⊢ ((Fun
𝑋 ∧ Fun 𝑌) → Fun (𝑋 ∘ 𝑌)) |
6 | 2, 4, 5 | mp2an 692 |
. 2
⊢ Fun
(𝑋 ∘ 𝑌) |
7 | | comptiunov2.z |
. . 3
⊢ 𝑍 = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘)) |
8 | 7 | funmpt2 6372 |
. 2
⊢ Fun 𝑍 |
9 | | ssv 3899 |
. . . . . . 7
⊢ ran 𝑌 ⊆ V |
10 | | comptiunov2.i |
. . . . . . . . 9
⊢ 𝐼 ∈ V |
11 | | ovex 7197 |
. . . . . . . . 9
⊢ (𝑎 ↑ 𝑖) ∈ V |
12 | 10, 11 | iunex 7687 |
. . . . . . . 8
⊢ ∪ 𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) ∈ V |
13 | 12, 1 | dmmpti 6475 |
. . . . . . 7
⊢ dom 𝑋 = V |
14 | 9, 13 | sseqtrri 3912 |
. . . . . 6
⊢ ran 𝑌 ⊆ dom 𝑋 |
15 | | dmcosseq 5810 |
. . . . . 6
⊢ (ran
𝑌 ⊆ dom 𝑋 → dom (𝑋 ∘ 𝑌) = dom 𝑌) |
16 | 14, 15 | ax-mp 5 |
. . . . 5
⊢ dom
(𝑋 ∘ 𝑌) = dom 𝑌 |
17 | | comptiunov2.j |
. . . . . . 7
⊢ 𝐽 ∈ V |
18 | | ovex 7197 |
. . . . . . 7
⊢ (𝑏 ↑ 𝑗) ∈ V |
19 | 17, 18 | iunex 7687 |
. . . . . 6
⊢ ∪ 𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) ∈ V |
20 | 19, 3 | dmmpti 6475 |
. . . . 5
⊢ dom 𝑌 = V |
21 | 16, 20 | eqtri 2761 |
. . . 4
⊢ dom
(𝑋 ∘ 𝑌) = V |
22 | | comptiunov2.k |
. . . . . . 7
⊢ 𝐾 = (𝐼 ∪ 𝐽) |
23 | 10, 17 | unex 7481 |
. . . . . . 7
⊢ (𝐼 ∪ 𝐽) ∈ V |
24 | 22, 23 | eqeltri 2829 |
. . . . . 6
⊢ 𝐾 ∈ V |
25 | | ovex 7197 |
. . . . . 6
⊢ (𝑐 ↑ 𝑘) ∈ V |
26 | 24, 25 | iunex 7687 |
. . . . 5
⊢ ∪ 𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) ∈ V |
27 | 26, 7 | dmmpti 6475 |
. . . 4
⊢ dom 𝑍 = V |
28 | 21, 27 | eqtr4i 2764 |
. . 3
⊢ dom
(𝑋 ∘ 𝑌) = dom 𝑍 |
29 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
30 | 29, 20 | eleqtrri 2832 |
. . . . . . . 8
⊢ 𝑑 ∈ dom 𝑌 |
31 | | fvco 6760 |
. . . . . . . 8
⊢ ((Fun
𝑌 ∧ 𝑑 ∈ dom 𝑌) → ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑))) |
32 | 4, 30, 31 | mp2an 692 |
. . . . . . 7
⊢ ((𝑋 ∘ 𝑌)‘𝑑) = (𝑋‘(𝑌‘𝑑)) |
33 | | oveq1 7171 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (𝑏 ↑ 𝑗) = (𝑑 ↑ 𝑗)) |
34 | 33 | iuneq2d 4907 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑑 → ∪
𝑗 ∈ 𝐽 (𝑏 ↑ 𝑗) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) |
35 | | ovex 7197 |
. . . . . . . . . . 11
⊢ (𝑑 ↑ 𝑗) ∈ V |
36 | 17, 35 | iunex 7687 |
. . . . . . . . . 10
⊢ ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V |
37 | 34, 3, 36 | fvmpt 6769 |
. . . . . . . . 9
⊢ (𝑑 ∈ V → (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) |
38 | 37 | elv 3403 |
. . . . . . . 8
⊢ (𝑌‘𝑑) = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) |
39 | 38 | fveq2i 6671 |
. . . . . . 7
⊢ (𝑋‘(𝑌‘𝑑)) = (𝑋‘∪
𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) |
40 | | oveq1 7171 |
. . . . . . . . . 10
⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → (𝑎 ↑ 𝑖) = (∪
𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)) |
41 | 40 | iuneq2d 4907 |
. . . . . . . . 9
⊢ (𝑎 = ∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) → ∪
𝑖 ∈ 𝐼 (𝑎 ↑ 𝑖) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)) |
42 | | ovex 7197 |
. . . . . . . . . 10
⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V |
43 | 10, 42 | iunex 7687 |
. . . . . . . . 9
⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ∈ V |
44 | 41, 1, 43 | fvmpt 6769 |
. . . . . . . 8
⊢ (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ∈ V → (𝑋‘∪
𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖)) |
45 | 36, 44 | ax-mp 5 |
. . . . . . 7
⊢ (𝑋‘∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗)) = ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
46 | 32, 39, 45 | 3eqtri 2765 |
. . . . . 6
⊢ ((𝑋 ∘ 𝑌)‘𝑑) = ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
47 | | oveq1 7171 |
. . . . . . . . 9
⊢ (𝑐 = 𝑑 → (𝑐 ↑ 𝑘) = (𝑑 ↑ 𝑘)) |
48 | 47 | iuneq2d 4907 |
. . . . . . . 8
⊢ (𝑐 = 𝑑 → ∪
𝑘 ∈ 𝐾 (𝑐 ↑ 𝑘) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
49 | | ovex 7197 |
. . . . . . . . 9
⊢ (𝑑 ↑ 𝑘) ∈ V |
50 | 24, 49 | iunex 7687 |
. . . . . . . 8
⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) ∈ V |
51 | 48, 7, 50 | fvmpt 6769 |
. . . . . . 7
⊢ (𝑑 ∈ V → (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
52 | 51 | elv 3403 |
. . . . . 6
⊢ (𝑍‘𝑑) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) |
53 | 46, 52 | eqeq12i 2753 |
. . . . 5
⊢ (((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
54 | 21, 53 | raleqbii 3146 |
. . . 4
⊢
(∀𝑑 ∈
dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) ↔ ∀𝑑 ∈ V ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
55 | | comptiunov2.3 |
. . . . . . 7
⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) ⊆ ∪
𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) |
56 | | iunxun 4976 |
. . . . . . . 8
⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) = (∪
𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪
𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘)) |
57 | | comptiunov2.1 |
. . . . . . . . 9
⊢ ∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ⊆ ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
58 | | comptiunov2.2 |
. . . . . . . . 9
⊢ ∪ 𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘) ⊆ ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
59 | 57, 58 | unssi 4073 |
. . . . . . . 8
⊢ (∪ 𝑘 ∈ 𝐼 (𝑑 ↑ 𝑘) ∪ ∪
𝑘 ∈ 𝐽 (𝑑 ↑ 𝑘)) ⊆ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
60 | 56, 59 | eqsstri 3909 |
. . . . . . 7
⊢ ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) ⊆ ∪
𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) |
61 | 55, 60 | eqssi 3891 |
. . . . . 6
⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) |
62 | | iuneq1 4894 |
. . . . . . 7
⊢ (𝐾 = (𝐼 ∪ 𝐽) → ∪
𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘)) |
63 | 22, 62 | ax-mp 5 |
. . . . . 6
⊢ ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) = ∪ 𝑘 ∈ (𝐼 ∪ 𝐽)(𝑑 ↑ 𝑘) |
64 | 61, 63 | eqtr4i 2764 |
. . . . 5
⊢ ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘) |
65 | 64 | a1i 11 |
. . . 4
⊢ (𝑑 ∈ V → ∪ 𝑖 ∈ 𝐼 (∪ 𝑗 ∈ 𝐽 (𝑑 ↑ 𝑗) ↑ 𝑖) = ∪ 𝑘 ∈ 𝐾 (𝑑 ↑ 𝑘)) |
66 | 54, 65 | mprgbir 3068 |
. . 3
⊢
∀𝑑 ∈ dom
(𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑) |
67 | | eqfunfv 6808 |
. . . 4
⊢ ((Fun
(𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((𝑋 ∘ 𝑌) = 𝑍 ↔ (dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)))) |
68 | 67 | biimprd 251 |
. . 3
⊢ ((Fun
(𝑋 ∘ 𝑌) ∧ Fun 𝑍) → ((dom (𝑋 ∘ 𝑌) = dom 𝑍 ∧ ∀𝑑 ∈ dom (𝑋 ∘ 𝑌)((𝑋 ∘ 𝑌)‘𝑑) = (𝑍‘𝑑)) → (𝑋 ∘ 𝑌) = 𝑍)) |
69 | 28, 66, 68 | mp2ani 698 |
. 2
⊢ ((Fun
(𝑋 ∘ 𝑌) ∧ Fun 𝑍) → (𝑋 ∘ 𝑌) = 𝑍) |
70 | 6, 8, 69 | mp2an 692 |
1
⊢ (𝑋 ∘ 𝑌) = 𝑍 |