Metamath Proof Explorer


Theorem txcmplem1

Description: Lemma for txcmp . (Contributed by Mario Carneiro, 14-Sep-2014)

Ref Expression
Hypotheses txcmp.x X = R
txcmp.y Y = S
txcmp.r φ R Comp
txcmp.s φ S Comp
txcmp.w φ W R × t S
txcmp.u φ X × Y = W
txcmp.a φ A Y
Assertion txcmplem1 φ u S A u v 𝒫 W Fin X × u v

Proof

Step Hyp Ref Expression
1 txcmp.x X = R
2 txcmp.y Y = S
3 txcmp.r φ R Comp
4 txcmp.s φ S Comp
5 txcmp.w φ W R × t S
6 txcmp.u φ X × Y = W
7 txcmp.a φ A Y
8 id x X x X
9 opelxpi x X A Y x A X × Y
10 8 7 9 syl2anr φ x X x A X × Y
11 6 adantr φ x X X × Y = W
12 10 11 eleqtrd φ x X x A W
13 eluni2 x A W k W x A k
14 12 13 sylib φ x X k W x A k
15 5 adantr φ x X W R × t S
16 15 sselda φ x X k W k R × t S
17 eltx R Comp S Comp k R × t S y k r R s S y r × s r × s k
18 3 4 17 syl2anc φ k R × t S y k r R s S y r × s r × s k
19 18 adantr φ x X k R × t S y k r R s S y r × s r × s k
20 19 biimpa φ x X k R × t S y k r R s S y r × s r × s k
21 16 20 syldan φ x X k W y k r R s S y r × s r × s k
22 eleq1 y = x A y r × s x A r × s
23 22 anbi1d y = x A y r × s r × s k x A r × s r × s k
24 23 2rexbidv y = x A r R s S y r × s r × s k r R s S x A r × s r × s k
25 24 rspccv y k r R s S y r × s r × s k x A k r R s S x A r × s r × s k
26 21 25 syl φ x X k W x A k r R s S x A r × s r × s k
27 opelxp1 x A r × s x r
28 27 ad2antrl φ x X k W x A r × s r × s k x r
29 opelxp2 x A r × s A s
30 29 ad2antrl φ x X k W x A r × s r × s k A s
31 30 snssd φ x X k W x A r × s r × s k A s
32 xpss2 A s r × A r × s
33 31 32 syl φ x X k W x A r × s r × s k r × A r × s
34 simprr φ x X k W x A r × s r × s k r × s k
35 33 34 sstrd φ x X k W x A r × s r × s k r × A k
36 28 35 jca φ x X k W x A r × s r × s k x r r × A k
37 36 ex φ x X k W x A r × s r × s k x r r × A k
38 37 rexlimdvw φ x X k W s S x A r × s r × s k x r r × A k
39 38 reximdv φ x X k W r R s S x A r × s r × s k r R x r r × A k
40 26 39 syld φ x X k W x A k r R x r r × A k
41 40 reximdva φ x X k W x A k k W r R x r r × A k
42 14 41 mpd φ x X k W r R x r r × A k
43 rexcom k W r R x r r × A k r R k W x r r × A k
44 r19.42v k W x r r × A k x r k W r × A k
45 44 rexbii r R k W x r r × A k r R x r k W r × A k
46 43 45 bitri k W r R x r r × A k r R x r k W r × A k
47 42 46 sylib φ x X r R x r k W r × A k
48 47 ralrimiva φ x X r R x r k W r × A k
49 sseq2 k = f r r × A k r × A f r
50 1 49 cmpcovf R Comp x X r R x r k W r × A k t 𝒫 R Fin X = t f f : t W r t r × A f r
51 3 48 50 syl2anc φ t 𝒫 R Fin X = t f f : t W r t r × A f r
52 3 ad2antrr φ t 𝒫 R Fin X = t f : t W r t r × A f r R Comp
53 cmptop S Comp S Top
54 4 53 syl φ S Top
55 54 ad2antrr φ t 𝒫 R Fin X = t f : t W r t r × A f r S Top
56 cmptop R Comp R Top
57 52 56 syl φ t 𝒫 R Fin X = t f : t W r t r × A f r R Top
58 txtop R Top S Top R × t S Top
59 57 55 58 syl2anc φ t 𝒫 R Fin X = t f : t W r t r × A f r R × t S Top
60 simprrl φ t 𝒫 R Fin X = t f : t W r t r × A f r f : t W
61 60 frnd φ t 𝒫 R Fin X = t f : t W r t r × A f r ran f W
62 5 ad2antrr φ t 𝒫 R Fin X = t f : t W r t r × A f r W R × t S
63 61 62 sstrd φ t 𝒫 R Fin X = t f : t W r t r × A f r ran f R × t S
64 uniopn R × t S Top ran f R × t S ran f R × t S
65 59 63 64 syl2anc φ t 𝒫 R Fin X = t f : t W r t r × A f r ran f R × t S
66 simprrr φ t 𝒫 R Fin X = t f : t W r t r × A f r r t r × A f r
67 ss2iun r t r × A f r r t r × A r t f r
68 66 67 syl φ t 𝒫 R Fin X = t f : t W r t r × A f r r t r × A r t f r
69 simprl φ t 𝒫 R Fin X = t f : t W r t r × A f r X = t
70 uniiun t = r t r
71 69 70 eqtrdi φ t 𝒫 R Fin X = t f : t W r t r × A f r X = r t r
72 71 xpeq1d φ t 𝒫 R Fin X = t f : t W r t r × A f r X × A = r t r × A
73 xpiundir r t r × A = r t r × A
74 72 73 eqtr2di φ t 𝒫 R Fin X = t f : t W r t r × A f r r t r × A = X × A
75 60 ffnd φ t 𝒫 R Fin X = t f : t W r t r × A f r f Fn t
76 fniunfv f Fn t r t f r = ran f
77 75 76 syl φ t 𝒫 R Fin X = t f : t W r t r × A f r r t f r = ran f
78 68 74 77 3sstr3d φ t 𝒫 R Fin X = t f : t W r t r × A f r X × A ran f
79 7 ad2antrr φ t 𝒫 R Fin X = t f : t W r t r × A f r A Y
80 1 2 52 55 65 78 79 txtube φ t 𝒫 R Fin X = t f : t W r t r × A f r u S A u X × u ran f
81 vex f V
82 81 rnex ran f V
83 82 elpw ran f 𝒫 W ran f W
84 61 83 sylibr φ t 𝒫 R Fin X = t f : t W r t r × A f r ran f 𝒫 W
85 simplr φ t 𝒫 R Fin X = t f : t W r t r × A f r t 𝒫 R Fin
86 85 elin2d φ t 𝒫 R Fin X = t f : t W r t r × A f r t Fin
87 dffn4 f Fn t f : t onto ran f
88 75 87 sylib φ t 𝒫 R Fin X = t f : t W r t r × A f r f : t onto ran f
89 fofi t Fin f : t onto ran f ran f Fin
90 86 88 89 syl2anc φ t 𝒫 R Fin X = t f : t W r t r × A f r ran f Fin
91 84 90 elind φ t 𝒫 R Fin X = t f : t W r t r × A f r ran f 𝒫 W Fin
92 unieq v = ran f v = ran f
93 92 sseq2d v = ran f X × u v X × u ran f
94 93 rspcev ran f 𝒫 W Fin X × u ran f v 𝒫 W Fin X × u v
95 94 ex ran f 𝒫 W Fin X × u ran f v 𝒫 W Fin X × u v
96 91 95 syl φ t 𝒫 R Fin X = t f : t W r t r × A f r X × u ran f v 𝒫 W Fin X × u v
97 96 anim2d φ t 𝒫 R Fin X = t f : t W r t r × A f r A u X × u ran f A u v 𝒫 W Fin X × u v
98 97 reximdv φ t 𝒫 R Fin X = t f : t W r t r × A f r u S A u X × u ran f u S A u v 𝒫 W Fin X × u v
99 80 98 mpd φ t 𝒫 R Fin X = t f : t W r t r × A f r u S A u v 𝒫 W Fin X × u v
100 99 expr φ t 𝒫 R Fin X = t f : t W r t r × A f r u S A u v 𝒫 W Fin X × u v
101 100 exlimdv φ t 𝒫 R Fin X = t f f : t W r t r × A f r u S A u v 𝒫 W Fin X × u v
102 101 expimpd φ t 𝒫 R Fin X = t f f : t W r t r × A f r u S A u v 𝒫 W Fin X × u v
103 102 rexlimdva φ t 𝒫 R Fin X = t f f : t W r t r × A f r u S A u v 𝒫 W Fin X × u v
104 51 103 mpd φ u S A u v 𝒫 W Fin X × u v