Metamath Proof Explorer

Theorem comptiunov2i

Description: The composition two indexed unions is sometimes a similar indexed union. (Contributed by RP, 10-Jun-2020)

Ref Expression
Hypotheses comptiunov2.x ⊢ X = a ∈ V ⟼ ⋃ i ∈ I a × ˙ i
comptiunov2.y ⊢ Y = b ∈ V ⟼ ⋃ j ∈ J b × ˙ j
comptiunov2.z ⊢ Z = c ∈ V ⟼ ⋃ k ∈ K c × ˙ k
comptiunov2.i ⊢ I ∈ V
comptiunov2.j ⊢ J ∈ V
comptiunov2.k ⊢ K = I ∪ J
comptiunov2.1 ⊢ ⋃ k ∈ I d × ˙ k ⊆ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
comptiunov2.2 ⊢ ⋃ k ∈ J d × ˙ k ⊆ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
comptiunov2.3 ⊢ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i ⊆ ⋃ k ∈ I ∪ J d × ˙ k
Assertion comptiunov2i ⊢ X ∘ Y = Z

Proof

Step Hyp Ref Expression
1 comptiunov2.x ⊢ X = a ∈ V ⟼ ⋃ i ∈ I a × ˙ i
2 comptiunov2.y ⊢ Y = b ∈ V ⟼ ⋃ j ∈ J b × ˙ j
3 comptiunov2.z ⊢ Z = c ∈ V ⟼ ⋃ k ∈ K c × ˙ k
4 comptiunov2.i ⊢ I ∈ V
5 comptiunov2.j ⊢ J ∈ V
6 comptiunov2.k ⊢ K = I ∪ J
7 comptiunov2.1 ⊢ ⋃ k ∈ I d × ˙ k ⊆ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
8 comptiunov2.2 ⊢ ⋃ k ∈ J d × ˙ k ⊆ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
9 comptiunov2.3 ⊢ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i ⊆ ⋃ k ∈ I ∪ J d × ˙ k
10 1 funmpt2 ⊢ Fun ⁡ X
11 2 funmpt2 ⊢ Fun ⁡ Y
12 funco ⊢ Fun ⁡ X ∧ Fun ⁡ Y → Fun ⁡ X ∘ Y
13 10 11 12 mp2an ⊢ Fun ⁡ X ∘ Y
14 3 funmpt2 ⊢ Fun ⁡ Z
15 ssv ⊢ ran ⁡ Y ⊆ V
16 ovex ⊢ a × ˙ i ∈ V
17 4 16 iunex ⊢ ⋃ i ∈ I a × ˙ i ∈ V
18 17 1 dmmpti ⊢ dom ⁡ X = V
19 15 18 sseqtrri ⊢ ran ⁡ Y ⊆ dom ⁡ X
20 dmcosseq ⊢ ran ⁡ Y ⊆ dom ⁡ X → dom ⁡ X ∘ Y = dom ⁡ Y
21 19 20 ax-mp ⊢ dom ⁡ X ∘ Y = dom ⁡ Y
22 ovex ⊢ b × ˙ j ∈ V
23 5 22 iunex ⊢ ⋃ j ∈ J b × ˙ j ∈ V
24 23 2 dmmpti ⊢ dom ⁡ Y = V
25 21 24 eqtri ⊢ dom ⁡ X ∘ Y = V
26 4 5 unex ⊢ I ∪ J ∈ V
27 6 26 eqeltri ⊢ K ∈ V
28 ovex ⊢ c × ˙ k ∈ V
29 27 28 iunex ⊢ ⋃ k ∈ K c × ˙ k ∈ V
30 29 3 dmmpti ⊢ dom ⁡ Z = V
31 25 30 eqtr4i ⊢ dom ⁡ X ∘ Y = dom ⁡ Z
32 vex ⊢ d ∈ V
33 32 24 eleqtrri ⊢ d ∈ dom ⁡ Y
34 fvco ⊢ Fun ⁡ Y ∧ d ∈ dom ⁡ Y → X ∘ Y ⁡ d = X ⁡ Y ⁡ d
35 11 33 34 mp2an ⊢ X ∘ Y ⁡ d = X ⁡ Y ⁡ d
36 oveq1 ⊢ b = d → b × ˙ j = d × ˙ j
37 36 iuneq2d ⊢ b = d → ⋃ j ∈ J b × ˙ j = ⋃ j ∈ J d × ˙ j
38 ovex ⊢ d × ˙ j ∈ V
39 5 38 iunex ⊢ ⋃ j ∈ J d × ˙ j ∈ V
40 37 2 39 fvmpt ⊢ d ∈ V → Y ⁡ d = ⋃ j ∈ J d × ˙ j
41 40 elv ⊢ Y ⁡ d = ⋃ j ∈ J d × ˙ j
42 41 fveq2i ⊢ X ⁡ Y ⁡ d = X ⁡ ⋃ j ∈ J d × ˙ j
43 oveq1 ⊢ a = ⋃ j ∈ J d × ˙ j → a × ˙ i = ⋃ j ∈ J d × ˙ j × ˙ i
44 43 iuneq2d ⊢ a = ⋃ j ∈ J d × ˙ j → ⋃ i ∈ I a × ˙ i = ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
45 ovex ⊢ ⋃ j ∈ J d × ˙ j × ˙ i ∈ V
46 4 45 iunex ⊢ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i ∈ V
47 44 1 46 fvmpt ⊢ ⋃ j ∈ J d × ˙ j ∈ V → X ⁡ ⋃ j ∈ J d × ˙ j = ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
48 39 47 ax-mp ⊢ X ⁡ ⋃ j ∈ J d × ˙ j = ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
49 35 42 48 3eqtri ⊢ X ∘ Y ⁡ d = ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
50 oveq1 ⊢ c = d → c × ˙ k = d × ˙ k
51 50 iuneq2d ⊢ c = d → ⋃ k ∈ K c × ˙ k = ⋃ k ∈ K d × ˙ k
52 ovex ⊢ d × ˙ k ∈ V
53 27 52 iunex ⊢ ⋃ k ∈ K d × ˙ k ∈ V
54 51 3 53 fvmpt ⊢ d ∈ V → Z ⁡ d = ⋃ k ∈ K d × ˙ k
55 54 elv ⊢ Z ⁡ d = ⋃ k ∈ K d × ˙ k
56 49 55 eqeq12i ⊢ X ∘ Y ⁡ d = Z ⁡ d ↔ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i = ⋃ k ∈ K d × ˙ k
57 25 56 raleqbii ⊢ ∀ d ∈ dom ⁡ X ∘ Y X ∘ Y ⁡ d = Z ⁡ d ↔ ∀ d ∈ V ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i = ⋃ k ∈ K d × ˙ k
58 iunxun ⊢ ⋃ k ∈ I ∪ J d × ˙ k = ⋃ k ∈ I d × ˙ k ∪ ⋃ k ∈ J d × ˙ k
59 7 8 unssi ⊢ ⋃ k ∈ I d × ˙ k ∪ ⋃ k ∈ J d × ˙ k ⊆ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
60 58 59 eqsstri ⊢ ⋃ k ∈ I ∪ J d × ˙ k ⊆ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i
61 9 60 eqssi ⊢ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i = ⋃ k ∈ I ∪ J d × ˙ k
62 iuneq1 ⊢ K = I ∪ J → ⋃ k ∈ K d × ˙ k = ⋃ k ∈ I ∪ J d × ˙ k
63 6 62 ax-mp ⊢ ⋃ k ∈ K d × ˙ k = ⋃ k ∈ I ∪ J d × ˙ k
64 61 63 eqtr4i ⊢ ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i = ⋃ k ∈ K d × ˙ k
65 64 a1i ⊢ d ∈ V → ⋃ i ∈ I ⋃ j ∈ J d × ˙ j × ˙ i = ⋃ k ∈ K d × ˙ k
66 57 65 mprgbir ⊢ ∀ d ∈ dom ⁡ X ∘ Y X ∘ Y ⁡ d = Z ⁡ d
67 eqfunfv ⊢ Fun ⁡ X ∘ Y ∧ Fun ⁡ Z → X ∘ Y = Z ↔ dom ⁡ X ∘ Y = dom ⁡ Z ∧ ∀ d ∈ dom ⁡ X ∘ Y X ∘ Y ⁡ d = Z ⁡ d
68 67 biimprd ⊢ Fun ⁡ X ∘ Y ∧ Fun ⁡ Z → dom ⁡ X ∘ Y = dom ⁡ Z ∧ ∀ d ∈ dom ⁡ X ∘ Y X ∘ Y ⁡ d = Z ⁡ d → X ∘ Y = Z
69 31 66 68 mp2ani ⊢ Fun ⁡ X ∘ Y ∧ Fun ⁡ Z → X ∘ Y = Z
70 13 14 69 mp2an ⊢ X ∘ Y = Z