Metamath Proof Explorer

Theorem txcmplem2

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×tS
txcmp.u ⊢φ→X×Y=⋃W
Assertion txcmplem2 ⊢φ→∃v∈𝒫W∩FinX×Y=⋃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×tS
6 txcmp.u ⊢φ→X×Y=⋃W
7 3 adantr ⊢φ∧x∈Y→R∈Comp
8 4 adantr ⊢φ∧x∈Y→S∈Comp
9 5 adantr ⊢φ∧x∈Y→W⊆R×tS
10 6 adantr ⊢φ∧x∈Y→X×Y=⋃W
11 simpr ⊢φ∧x∈Y→x∈Y
12 1 2 7 8 9 10 11 txcmplem1 ⊢φ∧x∈Y→∃u∈Sx∈u∧∃v∈𝒫W∩FinX×u⊆⋃v
13 12 ralrimiva ⊢φ→∀x∈Y∃u∈Sx∈u∧∃v∈𝒫W∩FinX×u⊆⋃v
14 unieq ⊢v=f⁡u→⋃v=⋃f⁡u
15 14 sseq2d ⊢v=f⁡u→X×u⊆⋃v↔X×u⊆⋃f⁡u
16 2 15 cmpcovf ⊢S∈Comp∧∀x∈Y∃u∈Sx∈u∧∃v∈𝒫W∩FinX×u⊆⋃v→∃w∈𝒫S∩FinY=⋃w∧∃ff:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u
17 4 13 16 syl2anc ⊢φ→∃w∈𝒫S∩FinY=⋃w∧∃ff:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u
18 simprrl ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→f:w⟶𝒫W∩Fin
19 ffn ⊢f:w⟶𝒫W∩Fin→fFnw
20 fniunfv ⊢fFnw→⋃z∈wf⁡z=⋃ran⁡f
21 18 19 20 3syl ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→⋃z∈wf⁡z=⋃ran⁡f
22 18 frnd ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→ran⁡f⊆𝒫W∩Fin
23 inss1 ⊢𝒫W∩Fin⊆𝒫W
24 22 23 sstrdi ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→ran⁡f⊆𝒫W
25 sspwuni ⊢ran⁡f⊆𝒫W↔⋃ran⁡f⊆W
26 24 25 sylib ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→⋃ran⁡f⊆W
27 21 26 eqsstrd ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→⋃z∈wf⁡z⊆W
28 vex ⊢w∈V
29 fvex ⊢f⁡z∈V
30 28 29 iunex ⊢⋃z∈wf⁡z∈V
31 30 elpw ⊢⋃z∈wf⁡z∈𝒫W↔⋃z∈wf⁡z⊆W
32 27 31 sylibr ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→⋃z∈wf⁡z∈𝒫W
33 inss2 ⊢𝒫S∩Fin⊆Fin
34 simplr ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→w∈𝒫S∩Fin
35 33 34 sselid ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→w∈Fin
36 inss2 ⊢𝒫W∩Fin⊆Fin
37 fss ⊢f:w⟶𝒫W∩Fin∧𝒫W∩Fin⊆Fin→f:w⟶Fin
38 18 36 37 sylancl ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→f:w⟶Fin
39 ffvelcdm ⊢f:w⟶Fin∧z∈w→f⁡z∈Fin
40 39 ralrimiva ⊢f:w⟶Fin→∀z∈wf⁡z∈Fin
41 38 40 syl ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∀z∈wf⁡z∈Fin
42 iunfi ⊢w∈Fin∧∀z∈wf⁡z∈Fin→⋃z∈wf⁡z∈Fin
43 35 41 42 syl2anc ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→⋃z∈wf⁡z∈Fin
44 32 43 elind ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→⋃z∈wf⁡z∈𝒫W∩Fin
45 simprl ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→Y=⋃w
46 uniiun ⊢⋃w=⋃z∈wz
47 45 46 eqtrdi ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→Y=⋃z∈wz
48 47 xpeq2d ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→X×Y=X×⋃z∈wz
49 xpiundi ⊢X×⋃z∈wz=⋃z∈wX×z
50 48 49 eqtrdi ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→X×Y=⋃z∈wX×z
51 simprrr ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∀u∈wX×u⊆⋃f⁡u
52 xpeq2 ⊢u=z→X×u=X×z
53 fveq2 ⊢u=z→f⁡u=f⁡z
54 53 unieqd ⊢u=z→⋃f⁡u=⋃f⁡z
55 52 54 sseq12d ⊢u=z→X×u⊆⋃f⁡u↔X×z⊆⋃f⁡z
56 55 cbvralvw ⊢∀u∈wX×u⊆⋃f⁡u↔∀z∈wX×z⊆⋃f⁡z
57 51 56 sylib ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∀z∈wX×z⊆⋃f⁡z
58 ss2iun ⊢∀z∈wX×z⊆⋃f⁡z→⋃z∈wX×z⊆⋃z∈w⋃f⁡z
59 57 58 syl ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→⋃z∈wX×z⊆⋃z∈w⋃f⁡z
60 50 59 eqsstrd ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→X×Y⊆⋃z∈w⋃f⁡z
61 18 ffvelcdmda ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u∧z∈w→f⁡z∈𝒫W∩Fin
62 23 61 sselid ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u∧z∈w→f⁡z∈𝒫W
63 elpwi ⊢f⁡z∈𝒫W→f⁡z⊆W
64 uniss ⊢f⁡z⊆W→⋃f⁡z⊆⋃W
65 62 63 64 3syl ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u∧z∈w→⋃f⁡z⊆⋃W
66 6 ad3antrrr ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u∧z∈w→X×Y=⋃W
67 65 66 sseqtrrd ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u∧z∈w→⋃f⁡z⊆X×Y
68 67 ralrimiva ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∀z∈w⋃f⁡z⊆X×Y
69 iunss ⊢⋃z∈w⋃f⁡z⊆X×Y↔∀z∈w⋃f⁡z⊆X×Y
70 68 69 sylibr ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→⋃z∈w⋃f⁡z⊆X×Y
71 60 70 eqssd ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→X×Y=⋃z∈w⋃f⁡z
72 iuncom4 ⊢⋃z∈w⋃f⁡z=⋃⋃z∈wf⁡z
73 71 72 eqtrdi ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→X×Y=⋃⋃z∈wf⁡z
74 unieq ⊢v=⋃z∈wf⁡z→⋃v=⋃⋃z∈wf⁡z
75 74 rspceeqv ⊢⋃z∈wf⁡z∈𝒫W∩Fin∧X×Y=⋃⋃z∈wf⁡z→∃v∈𝒫W∩FinX×Y=⋃v
76 44 73 75 syl2anc ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w∧f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∃v∈𝒫W∩FinX×Y=⋃v
77 76 expr ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w→f:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∃v∈𝒫W∩FinX×Y=⋃v
78 77 exlimdv ⊢φ∧w∈𝒫S∩Fin∧Y=⋃w→∃ff:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∃v∈𝒫W∩FinX×Y=⋃v
79 78 expimpd ⊢φ∧w∈𝒫S∩Fin→Y=⋃w∧∃ff:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∃v∈𝒫W∩FinX×Y=⋃v
80 79 rexlimdva ⊢φ→∃w∈𝒫S∩FinY=⋃w∧∃ff:w⟶𝒫W∩Fin∧∀u∈wX×u⊆⋃f⁡u→∃v∈𝒫W∩FinX×Y=⋃v
81 17 80 mpd ⊢φ→∃v∈𝒫W∩FinX×Y=⋃v