Metamath Proof Explorer

Theorem txcmplem2

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

Ref Expression
Hypotheses txcmp.x ⊢ 𝑋 = ∪ 𝑅
txcmp.y ⊢ 𝑌 = ∪ 𝑆
txcmp.r ⊢ ( 𝜑 → 𝑅 ∈ Comp )
txcmp.s ⊢ ( 𝜑 → 𝑆 ∈ Comp )
txcmp.w ⊢ ( 𝜑 → 𝑊 ⊆ ( 𝑅 ×t 𝑆 ) )
txcmp.u ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ∪ 𝑊 )
Assertion txcmplem2 ( 𝜑 → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑌 ) = ∪ 𝑣 )

Proof

Step Hyp Ref Expression
1 txcmp.x ⊢ 𝑋 = ∪ 𝑅
2 txcmp.y ⊢ 𝑌 = ∪ 𝑆
3 txcmp.r ⊢ ( 𝜑 → 𝑅 ∈ Comp )
4 txcmp.s ⊢ ( 𝜑 → 𝑆 ∈ Comp )
5 txcmp.w ⊢ ( 𝜑 → 𝑊 ⊆ ( 𝑅 ×t 𝑆 ) )
6 txcmp.u ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ∪ 𝑊 )
7 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑅 ∈ Comp )
8 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑆 ∈ Comp )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑊 ⊆ ( 𝑅 ×t 𝑆 ) )
10 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑋 × 𝑌 ) = ∪ 𝑊 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑌 )
12 1 2 7 8 9 10 11 txcmplem1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∃ 𝑢 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) )
13 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑌 ∃ 𝑢 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) )
14 unieq ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ∪ 𝑣 = ∪ ( 𝑓 ‘ 𝑢 ) )
15 14 sseq2d ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ↔ ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) )
16 2 15 cmpcovf ⊢ ( ( 𝑆 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑌 ∃ 𝑢 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) ) → ∃ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝑌 = ∪ 𝑤 ∧ ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) )
17 4 13 16 syl2anc ⊢ ( 𝜑 → ∃ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝑌 = ∪ 𝑤 ∧ ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) )
18 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) )
19 ffn ⊢ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) → 𝑓 Fn 𝑤 )
20 fniunfv ⊢ ( 𝑓 Fn 𝑤 → ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) = ∪ ran 𝑓 )
21 18 19 20 3syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) = ∪ ran 𝑓 )
22 18 frnd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ran 𝑓 ⊆ ( 𝒫 𝑊 ∩ Fin ) )
23 inss1 ⊢ ( 𝒫 𝑊 ∩ Fin ) ⊆ 𝒫 𝑊
24 22 23 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ran 𝑓 ⊆ 𝒫 𝑊 )
25 sspwuni ⊢ ( ran 𝑓 ⊆ 𝒫 𝑊 ↔ ∪ ran 𝑓 ⊆ 𝑊 )
26 24 25 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∪ ran 𝑓 ⊆ 𝑊 )
27 21 26 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ⊆ 𝑊 )
28 vex ⊢ 𝑤 ∈ V
29 fvex ⊢ ( 𝑓 ‘ 𝑧 ) ∈ V
30 28 29 iunex ⊢ ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ V
31 30 elpw ⊢ ( ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ 𝒫 𝑊 ↔ ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ⊆ 𝑊 )
32 27 31 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ 𝒫 𝑊 )
33 inss2 ⊢ ( 𝒫 𝑆 ∩ Fin ) ⊆ Fin
34 simplr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) )
35 33 34 sselid ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → 𝑤 ∈ Fin )
36 inss2 ⊢ ( 𝒫 𝑊 ∩ Fin ) ⊆ Fin
37 fss ⊢ ( ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝒫 𝑊 ∩ Fin ) ⊆ Fin ) → 𝑓 : 𝑤 ⟶ Fin )
38 18 36 37 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → 𝑓 : 𝑤 ⟶ Fin )
39 ffvelcdm ⊢ ( ( 𝑓 : 𝑤 ⟶ Fin ∧ 𝑧 ∈ 𝑤 ) → ( 𝑓 ‘ 𝑧 ) ∈ Fin )
40 39 ralrimiva ⊢ ( 𝑓 : 𝑤 ⟶ Fin → ∀ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ Fin )
41 38 40 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∀ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ Fin )
42 iunfi ⊢ ( ( 𝑤 ∈ Fin ∧ ∀ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ Fin ) → ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ Fin )
43 35 41 42 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ Fin )
44 32 43 elind ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ ( 𝒫 𝑊 ∩ Fin ) )
45 simprl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → 𝑌 = ∪ 𝑤 )
46 uniiun ⊢ ∪ 𝑤 = ∪ 𝑧 ∈ 𝑤 𝑧
47 45 46 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → 𝑌 = ∪ 𝑧 ∈ 𝑤 𝑧 )
48 47 xpeq2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ( 𝑋 × 𝑌 ) = ( 𝑋 × ∪ 𝑧 ∈ 𝑤 𝑧 ) )
49 xpiundi ⊢ ( 𝑋 × ∪ 𝑧 ∈ 𝑤 𝑧 ) = ∪ 𝑧 ∈ 𝑤 ( 𝑋 × 𝑧 )
50 48 49 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ( 𝑋 × 𝑌 ) = ∪ 𝑧 ∈ 𝑤 ( 𝑋 × 𝑧 ) )
51 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) )
52 xpeq2 ⊢ ( 𝑢 = 𝑧 → ( 𝑋 × 𝑢 ) = ( 𝑋 × 𝑧 ) )
53 fveq2 ⊢ ( 𝑢 = 𝑧 → ( 𝑓 ‘ 𝑢 ) = ( 𝑓 ‘ 𝑧 ) )
54 53 unieqd ⊢ ( 𝑢 = 𝑧 → ∪ ( 𝑓 ‘ 𝑢 ) = ∪ ( 𝑓 ‘ 𝑧 ) )
55 52 54 sseq12d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ↔ ( 𝑋 × 𝑧 ) ⊆ ∪ ( 𝑓 ‘ 𝑧 ) ) )
56 55 cbvralvw ⊢ ( ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ↔ ∀ 𝑧 ∈ 𝑤 ( 𝑋 × 𝑧 ) ⊆ ∪ ( 𝑓 ‘ 𝑧 ) )
57 51 56 sylib ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∀ 𝑧 ∈ 𝑤 ( 𝑋 × 𝑧 ) ⊆ ∪ ( 𝑓 ‘ 𝑧 ) )
58 ss2iun ⊢ ( ∀ 𝑧 ∈ 𝑤 ( 𝑋 × 𝑧 ) ⊆ ∪ ( 𝑓 ‘ 𝑧 ) → ∪ 𝑧 ∈ 𝑤 ( 𝑋 × 𝑧 ) ⊆ ∪ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) )
59 57 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∪ 𝑧 ∈ 𝑤 ( 𝑋 × 𝑧 ) ⊆ ∪ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) )
60 50 59 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ( 𝑋 × 𝑌 ) ⊆ ∪ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) )
61 18 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) ∧ 𝑧 ∈ 𝑤 ) → ( 𝑓 ‘ 𝑧 ) ∈ ( 𝒫 𝑊 ∩ Fin ) )
62 23 61 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) ∧ 𝑧 ∈ 𝑤 ) → ( 𝑓 ‘ 𝑧 ) ∈ 𝒫 𝑊 )
63 elpwi ⊢ ( ( 𝑓 ‘ 𝑧 ) ∈ 𝒫 𝑊 → ( 𝑓 ‘ 𝑧 ) ⊆ 𝑊 )
64 uniss ⊢ ( ( 𝑓 ‘ 𝑧 ) ⊆ 𝑊 → ∪ ( 𝑓 ‘ 𝑧 ) ⊆ ∪ 𝑊 )
65 62 63 64 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) ∧ 𝑧 ∈ 𝑤 ) → ∪ ( 𝑓 ‘ 𝑧 ) ⊆ ∪ 𝑊 )
66 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) ∧ 𝑧 ∈ 𝑤 ) → ( 𝑋 × 𝑌 ) = ∪ 𝑊 )
67 65 66 sseqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) ∧ 𝑧 ∈ 𝑤 ) → ∪ ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝑋 × 𝑌 ) )
68 67 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∀ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝑋 × 𝑌 ) )
69 iunss ⊢ ( ∪ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝑋 × 𝑌 ) ↔ ∀ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝑋 × 𝑌 ) )
70 68 69 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∪ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) ⊆ ( 𝑋 × 𝑌 ) )
71 60 70 eqssd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ( 𝑋 × 𝑌 ) = ∪ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) )
72 iuncom4 ⊢ ∪ 𝑧 ∈ 𝑤 ∪ ( 𝑓 ‘ 𝑧 ) = ∪ ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 )
73 71 72 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ( 𝑋 × 𝑌 ) = ∪ ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) )
74 unieq ⊢ ( 𝑣 = ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) → ∪ 𝑣 = ∪ ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) )
75 74 rspceeqv ⊢ ( ( ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑋 × 𝑌 ) = ∪ ∪ 𝑧 ∈ 𝑤 ( 𝑓 ‘ 𝑧 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑌 ) = ∪ 𝑣 )
76 44 73 75 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ ( 𝑌 = ∪ 𝑤 ∧ ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑌 ) = ∪ 𝑣 )
77 76 expr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ 𝑌 = ∪ 𝑤 ) → ( ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑌 ) = ∪ 𝑣 ) )
78 77 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) ∧ 𝑌 = ∪ 𝑤 ) → ( ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑌 ) = ∪ 𝑣 ) )
79 78 expimpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ) → ( ( 𝑌 = ∪ 𝑤 ∧ ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑌 ) = ∪ 𝑣 ) )
80 79 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝑌 = ∪ 𝑤 ∧ ∃ 𝑓 ( 𝑓 : 𝑤 ⟶ ( 𝒫 𝑊 ∩ Fin ) ∧ ∀ 𝑢 ∈ 𝑤 ( 𝑋 × 𝑢 ) ⊆ ∪ ( 𝑓 ‘ 𝑢 ) ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑌 ) = ∪ 𝑣 ) )
81 17 80 mpd ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑌 ) = ∪ 𝑣 )