Metamath Proof Explorer


Theorem prodmo

Description: A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 F = k if k A B 1
prodmo.2 φ k A B
prodmo.3 G = j f j / k B
Assertion prodmo φ * x m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A x = seq 1 × G m

Proof

Step Hyp Ref Expression
1 prodmo.1 F = k if k A B 1
2 prodmo.2 φ k A B
3 prodmo.3 G = j f j / k B
4 3simpb A m n m y y 0 seq n × F y seq m × F x A m seq m × F x
5 4 reximi m A m n m y y 0 seq n × F y seq m × F x m A m seq m × F x
6 3simpb A m n m y y 0 seq n × F y seq m × F z A m seq m × F z
7 6 reximi m A m n m y y 0 seq n × F y seq m × F z m A m seq m × F z
8 fveq2 m = w m = w
9 8 sseq2d m = w A m A w
10 seqeq1 m = w seq m × F = seq w × F
11 10 breq1d m = w seq m × F z seq w × F z
12 9 11 anbi12d m = w A m seq m × F z A w seq w × F z
13 12 cbvrexvw m A m seq m × F z w A w seq w × F z
14 13 anbi2i m A m seq m × F x m A m seq m × F z m A m seq m × F x w A w seq w × F z
15 reeanv m w A m seq m × F x A w seq w × F z m A m seq m × F x w A w seq w × F z
16 14 15 bitr4i m A m seq m × F x m A m seq m × F z m w A m seq m × F x A w seq w × F z
17 simprlr m w A m seq m × F x A w seq w × F z seq m × F x
18 17 adantl φ m w A m seq m × F x A w seq w × F z seq m × F x
19 2 adantlr φ m w A m seq m × F x A w seq w × F z k A B
20 simprll φ m w A m seq m × F x A w seq w × F z m
21 simprlr φ m w A m seq m × F x A w seq w × F z w
22 simprll m w A m seq m × F x A w seq w × F z A m
23 22 adantl φ m w A m seq m × F x A w seq w × F z A m
24 simprrl m w A m seq m × F x A w seq w × F z A w
25 24 adantl φ m w A m seq m × F x A w seq w × F z A w
26 1 19 20 21 23 25 prodrb φ m w A m seq m × F x A w seq w × F z seq m × F x seq w × F x
27 18 26 mpbid φ m w A m seq m × F x A w seq w × F z seq w × F x
28 simprrr m w A m seq m × F x A w seq w × F z seq w × F z
29 28 adantl φ m w A m seq m × F x A w seq w × F z seq w × F z
30 climuni seq w × F x seq w × F z x = z
31 27 29 30 syl2anc φ m w A m seq m × F x A w seq w × F z x = z
32 31 expcom m w A m seq m × F x A w seq w × F z φ x = z
33 32 ex m w A m seq m × F x A w seq w × F z φ x = z
34 33 rexlimivv m w A m seq m × F x A w seq w × F z φ x = z
35 16 34 sylbi m A m seq m × F x m A m seq m × F z φ x = z
36 5 7 35 syl2an m A m n m y y 0 seq n × F y seq m × F x m A m n m y y 0 seq n × F y seq m × F z φ x = z
37 1 2 3 prodmolem2 φ m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A x = seq 1 × G m z = x
38 equcomi z = x x = z
39 37 38 syl6 φ m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A x = seq 1 × G m x = z
40 39 expimpd φ m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A x = seq 1 × G m x = z
41 40 com12 m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A x = seq 1 × G m φ x = z
42 41 ancoms m f f : 1 m 1-1 onto A x = seq 1 × G m m A m n m y y 0 seq n × F y seq m × F z φ x = z
43 1 2 3 prodmolem2 φ m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A z = seq 1 × G m x = z
44 43 expimpd φ m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A z = seq 1 × G m x = z
45 44 com12 m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A z = seq 1 × G m φ x = z
46 reeanv m w f f : 1 m 1-1 onto A x = seq 1 × G m g g : 1 w 1-1 onto A z = seq 1 × j g j / k B w m f f : 1 m 1-1 onto A x = seq 1 × G m w g g : 1 w 1-1 onto A z = seq 1 × j g j / k B w
47 exdistrv f g f : 1 m 1-1 onto A x = seq 1 × G m g : 1 w 1-1 onto A z = seq 1 × j g j / k B w f f : 1 m 1-1 onto A x = seq 1 × G m g g : 1 w 1-1 onto A z = seq 1 × j g j / k B w
48 47 2rexbii m w f g f : 1 m 1-1 onto A x = seq 1 × G m g : 1 w 1-1 onto A z = seq 1 × j g j / k B w m w f f : 1 m 1-1 onto A x = seq 1 × G m g g : 1 w 1-1 onto A z = seq 1 × j g j / k B w
49 oveq2 m = w 1 m = 1 w
50 49 f1oeq2d m = w f : 1 m 1-1 onto A f : 1 w 1-1 onto A
51 fveq2 m = w seq 1 × G m = seq 1 × G w
52 51 eqeq2d m = w z = seq 1 × G m z = seq 1 × G w
53 50 52 anbi12d m = w f : 1 m 1-1 onto A z = seq 1 × G m f : 1 w 1-1 onto A z = seq 1 × G w
54 53 exbidv m = w f f : 1 m 1-1 onto A z = seq 1 × G m f f : 1 w 1-1 onto A z = seq 1 × G w
55 f1oeq1 f = g f : 1 w 1-1 onto A g : 1 w 1-1 onto A
56 fveq1 f = g f j = g j
57 56 csbeq1d f = g f j / k B = g j / k B
58 57 mpteq2dv f = g j f j / k B = j g j / k B
59 3 58 syl5eq f = g G = j g j / k B
60 59 seqeq3d f = g seq 1 × G = seq 1 × j g j / k B
61 60 fveq1d f = g seq 1 × G w = seq 1 × j g j / k B w
62 61 eqeq2d f = g z = seq 1 × G w z = seq 1 × j g j / k B w
63 55 62 anbi12d f = g f : 1 w 1-1 onto A z = seq 1 × G w g : 1 w 1-1 onto A z = seq 1 × j g j / k B w
64 63 cbvexvw f f : 1 w 1-1 onto A z = seq 1 × G w g g : 1 w 1-1 onto A z = seq 1 × j g j / k B w
65 54 64 syl6bb m = w f f : 1 m 1-1 onto A z = seq 1 × G m g g : 1 w 1-1 onto A z = seq 1 × j g j / k B w
66 65 cbvrexvw m f f : 1 m 1-1 onto A z = seq 1 × G m w g g : 1 w 1-1 onto A z = seq 1 × j g j / k B w
67 66 anbi2i m f f : 1 m 1-1 onto A x = seq 1 × G m m f f : 1 m 1-1 onto A z = seq 1 × G m m f f : 1 m 1-1 onto A x = seq 1 × G m w g g : 1 w 1-1 onto A z = seq 1 × j g j / k B w
68 46 48 67 3bitr4i m w f g f : 1 m 1-1 onto A x = seq 1 × G m g : 1 w 1-1 onto A z = seq 1 × j g j / k B w m f f : 1 m 1-1 onto A x = seq 1 × G m m f f : 1 m 1-1 onto A z = seq 1 × G m
69 an4 f : 1 m 1-1 onto A x = seq 1 × G m g : 1 w 1-1 onto A z = seq 1 × j g j / k B w f : 1 m 1-1 onto A g : 1 w 1-1 onto A x = seq 1 × G m z = seq 1 × j g j / k B w
70 2 ad4ant14 φ m w f : 1 m 1-1 onto A g : 1 w 1-1 onto A k A B
71 fveq2 j = a f j = f a
72 71 csbeq1d j = a f j / k B = f a / k B
73 72 cbvmptv j f j / k B = a f a / k B
74 3 73 eqtri G = a f a / k B
75 fveq2 j = a g j = g a
76 75 csbeq1d j = a g j / k B = g a / k B
77 76 cbvmptv j g j / k B = a g a / k B
78 simplr φ m w f : 1 m 1-1 onto A g : 1 w 1-1 onto A m w
79 simprl φ m w f : 1 m 1-1 onto A g : 1 w 1-1 onto A f : 1 m 1-1 onto A
80 simprr φ m w f : 1 m 1-1 onto A g : 1 w 1-1 onto A g : 1 w 1-1 onto A
81 1 70 74 77 78 79 80 prodmolem3 φ m w f : 1 m 1-1 onto A g : 1 w 1-1 onto A seq 1 × G m = seq 1 × j g j / k B w
82 eqeq12 x = seq 1 × G m z = seq 1 × j g j / k B w x = z seq 1 × G m = seq 1 × j g j / k B w
83 81 82 syl5ibrcom φ m w f : 1 m 1-1 onto A g : 1 w 1-1 onto A x = seq 1 × G m z = seq 1 × j g j / k B w x = z
84 83 expimpd φ m w f : 1 m 1-1 onto A g : 1 w 1-1 onto A x = seq 1 × G m z = seq 1 × j g j / k B w x = z
85 69 84 syl5bi φ m w f : 1 m 1-1 onto A x = seq 1 × G m g : 1 w 1-1 onto A z = seq 1 × j g j / k B w x = z
86 85 exlimdvv φ m w f g f : 1 m 1-1 onto A x = seq 1 × G m g : 1 w 1-1 onto A z = seq 1 × j g j / k B w x = z
87 86 rexlimdvva φ m w f g f : 1 m 1-1 onto A x = seq 1 × G m g : 1 w 1-1 onto A z = seq 1 × j g j / k B w x = z
88 68 87 syl5bir φ m f f : 1 m 1-1 onto A x = seq 1 × G m m f f : 1 m 1-1 onto A z = seq 1 × G m x = z
89 88 com12 m f f : 1 m 1-1 onto A x = seq 1 × G m m f f : 1 m 1-1 onto A z = seq 1 × G m φ x = z
90 36 42 45 89 ccase m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A x = seq 1 × G m m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A z = seq 1 × G m φ x = z
91 90 com12 φ m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A x = seq 1 × G m m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A z = seq 1 × G m x = z
92 91 alrimivv φ x z m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A x = seq 1 × G m m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A z = seq 1 × G m x = z
93 breq2 x = z seq m × F x seq m × F z
94 93 3anbi3d x = z A m n m y y 0 seq n × F y seq m × F x A m n m y y 0 seq n × F y seq m × F z
95 94 rexbidv x = z m A m n m y y 0 seq n × F y seq m × F x m A m n m y y 0 seq n × F y seq m × F z
96 eqeq1 x = z x = seq 1 × G m z = seq 1 × G m
97 96 anbi2d x = z f : 1 m 1-1 onto A x = seq 1 × G m f : 1 m 1-1 onto A z = seq 1 × G m
98 97 exbidv x = z f f : 1 m 1-1 onto A x = seq 1 × G m f f : 1 m 1-1 onto A z = seq 1 × G m
99 98 rexbidv x = z m f f : 1 m 1-1 onto A x = seq 1 × G m m f f : 1 m 1-1 onto A z = seq 1 × G m
100 95 99 orbi12d x = z m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A x = seq 1 × G m m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A z = seq 1 × G m
101 100 mo4 * x m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A x = seq 1 × G m x z m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A x = seq 1 × G m m A m n m y y 0 seq n × F y seq m × F z m f f : 1 m 1-1 onto A z = seq 1 × G m x = z
102 92 101 sylibr φ * x m A m n m y y 0 seq n × F y seq m × F x m f f : 1 m 1-1 onto A x = seq 1 × G m