Metamath Proof Explorer

Theorem txcmplem1

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 ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ∪ 𝑊 )
txcmp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑌 )
Assertion txcmplem1 ( 𝜑 → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ 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 txcmp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑌 )
8 id ⊢ ( 𝑥 ∈ 𝑋 → 𝑥 ∈ 𝑋 )
9 opelxpi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑋 × 𝑌 ) )
10 8 7 9 syl2anr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑋 × 𝑌 ) )
11 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 × 𝑌 ) = ∪ 𝑊 )
12 10 11 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑥 , 𝐴 ⟩ ∈ ∪ 𝑊 )
13 eluni2 ⊢ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ∪ 𝑊 ↔ ∃ 𝑘 ∈ 𝑊 ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝑘 )
14 12 13 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑘 ∈ 𝑊 ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝑘 )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑊 ⊆ ( 𝑅 ×t 𝑆 ) )
16 15 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ ( 𝑅 ×t 𝑆 ) )
17 eltx ⊢ ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Comp ) → ( 𝑘 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑘 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) )
18 3 4 17 syl2anc ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑘 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑘 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) )
20 19 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ ( 𝑅 ×t 𝑆 ) ) → ∀ 𝑦 ∈ 𝑘 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) )
21 16 20 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) → ∀ 𝑦 ∈ 𝑘 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) )
22 eleq1 ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐴 ⟩ → ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ↔ ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ) )
23 22 anbi1d ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐴 ⟩ → ( ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ↔ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) )
24 23 2rexbidv ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐴 ⟩ → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) )
25 24 rspccv ⊢ ( ∀ 𝑦 ∈ 𝑘 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) → ( ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝑘 → ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) )
26 21 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) → ( ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝑘 → ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) )
27 opelxp1 ⊢ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) → 𝑥 ∈ 𝑟 )
28 27 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) ∧ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) → 𝑥 ∈ 𝑟 )
29 opelxp2 ⊢ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) → 𝐴 ∈ 𝑠 )
30 29 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) ∧ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) → 𝐴 ∈ 𝑠 )
31 30 snssd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) ∧ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) → { 𝐴 } ⊆ 𝑠 )
32 xpss2 ⊢ ( { 𝐴 } ⊆ 𝑠 → ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑟 × 𝑠 ) )
33 31 32 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) ∧ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) → ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑟 × 𝑠 ) )
34 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) ∧ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) → ( 𝑟 × 𝑠 ) ⊆ 𝑘 )
35 33 34 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) ∧ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) → ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 )
36 28 35 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) ∧ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) ) → ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) )
37 36 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) → ( ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) → ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ) )
38 37 rexlimdvw ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) → ( ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) → ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ) )
39 38 reximdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑘 ) → ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ) )
40 26 39 syld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝑊 ) → ( ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝑘 → ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ) )
41 40 reximdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∃ 𝑘 ∈ 𝑊 ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝑘 → ∃ 𝑘 ∈ 𝑊 ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ) )
42 14 41 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑘 ∈ 𝑊 ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) )
43 rexcom ⊢ ( ∃ 𝑘 ∈ 𝑊 ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑘 ∈ 𝑊 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) )
44 r19.42v ⊢ ( ∃ 𝑘 ∈ 𝑊 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ↔ ( 𝑥 ∈ 𝑟 ∧ ∃ 𝑘 ∈ 𝑊 ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) )
45 44 rexbii ⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑘 ∈ 𝑊 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ↔ ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ∃ 𝑘 ∈ 𝑊 ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) )
46 43 45 bitri ⊢ ( ∃ 𝑘 ∈ 𝑊 ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ↔ ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ∃ 𝑘 ∈ 𝑊 ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) )
47 42 46 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ∃ 𝑘 ∈ 𝑊 ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) )
48 47 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ∃ 𝑘 ∈ 𝑊 ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) )
49 sseq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑟 ) → ( ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ↔ ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) )
50 1 49 cmpcovf ⊢ ( ( 𝑅 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑟 ∈ 𝑅 ( 𝑥 ∈ 𝑟 ∧ ∃ 𝑘 ∈ 𝑊 ( 𝑟 × { 𝐴 } ) ⊆ 𝑘 ) ) → ∃ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ( 𝑋 = ∪ 𝑡 ∧ ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) )
51 3 48 50 syl2anc ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ( 𝑋 = ∪ 𝑡 ∧ ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) )
52 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑅 ∈ Comp )
53 cmptop ⊢ ( 𝑆 ∈ Comp → 𝑆 ∈ Top )
54 4 53 syl ⊢ ( 𝜑 → 𝑆 ∈ Top )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑆 ∈ Top )
56 cmptop ⊢ ( 𝑅 ∈ Comp → 𝑅 ∈ Top )
57 52 56 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑅 ∈ Top )
58 txtop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
59 57 55 58 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
60 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑓 : 𝑡 ⟶ 𝑊 )
61 60 frnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ran 𝑓 ⊆ 𝑊 )
62 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑊 ⊆ ( 𝑅 ×t 𝑆 ) )
63 61 62 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ran 𝑓 ⊆ ( 𝑅 ×t 𝑆 ) )
64 uniopn ⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ran 𝑓 ⊆ ( 𝑅 ×t 𝑆 ) ) → ∪ ran 𝑓 ∈ ( 𝑅 ×t 𝑆 ) )
65 59 63 64 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ∪ ran 𝑓 ∈ ( 𝑅 ×t 𝑆 ) )
66 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) )
67 ss2iun ⊢ ( ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) → ∪ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ∪ 𝑟 ∈ 𝑡 ( 𝑓 ‘ 𝑟 ) )
68 66 67 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ∪ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ∪ 𝑟 ∈ 𝑡 ( 𝑓 ‘ 𝑟 ) )
69 simprl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑋 = ∪ 𝑡 )
70 uniiun ⊢ ∪ 𝑡 = ∪ 𝑟 ∈ 𝑡 𝑟
71 69 70 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑋 = ∪ 𝑟 ∈ 𝑡 𝑟 )
72 71 xpeq1d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ( 𝑋 × { 𝐴 } ) = ( ∪ 𝑟 ∈ 𝑡 𝑟 × { 𝐴 } ) )
73 xpiundir ⊢ ( ∪ 𝑟 ∈ 𝑡 𝑟 × { 𝐴 } ) = ∪ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } )
74 72 73 eqtr2di ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ∪ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) = ( 𝑋 × { 𝐴 } ) )
75 60 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑓 Fn 𝑡 )
76 fniunfv ⊢ ( 𝑓 Fn 𝑡 → ∪ 𝑟 ∈ 𝑡 ( 𝑓 ‘ 𝑟 ) = ∪ ran 𝑓 )
77 75 76 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ∪ 𝑟 ∈ 𝑡 ( 𝑓 ‘ 𝑟 ) = ∪ ran 𝑓 )
78 68 74 77 3sstr3d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ( 𝑋 × { 𝐴 } ) ⊆ ∪ ran 𝑓 )
79 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝐴 ∈ 𝑌 )
80 1 2 52 55 65 78 79 txtube ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ ∪ ran 𝑓 ) )
81 vex ⊢ 𝑓 ∈ V
82 81 rnex ⊢ ran 𝑓 ∈ V
83 82 elpw ⊢ ( ran 𝑓 ∈ 𝒫 𝑊 ↔ ran 𝑓 ⊆ 𝑊 )
84 61 83 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ran 𝑓 ∈ 𝒫 𝑊 )
85 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) )
86 85 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑡 ∈ Fin )
87 dffn4 ⊢ ( 𝑓 Fn 𝑡 ↔ 𝑓 : 𝑡 –onto→ ran 𝑓 )
88 75 87 sylib ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → 𝑓 : 𝑡 –onto→ ran 𝑓 )
89 fofi ⊢ ( ( 𝑡 ∈ Fin ∧ 𝑓 : 𝑡 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
90 86 88 89 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ran 𝑓 ∈ Fin )
91 84 90 elind ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ran 𝑓 ∈ ( 𝒫 𝑊 ∩ Fin ) )
92 unieq ⊢ ( 𝑣 = ran 𝑓 → ∪ 𝑣 = ∪ ran 𝑓 )
93 92 sseq2d ⊢ ( 𝑣 = ran 𝑓 → ( ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ↔ ( 𝑋 × 𝑢 ) ⊆ ∪ ran 𝑓 ) )
94 93 rspcev ⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑊 ∩ Fin ) ∧ ( 𝑋 × 𝑢 ) ⊆ ∪ ran 𝑓 ) → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 )
95 94 ex ⊢ ( ran 𝑓 ∈ ( 𝒫 𝑊 ∩ Fin ) → ( ( 𝑋 × 𝑢 ) ⊆ ∪ ran 𝑓 → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) )
96 91 95 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ( ( 𝑋 × 𝑢 ) ⊆ ∪ ran 𝑓 → ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) )
97 96 anim2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ( ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ ∪ ran 𝑓 ) → ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) ) )
98 97 reximdv ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ( ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ ∪ ran 𝑓 ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) ) )
99 80 98 mpd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) )
100 99 expr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ 𝑋 = ∪ 𝑡 ) → ( ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) ) )
101 100 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ 𝑋 = ∪ 𝑡 ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) ) )
102 101 expimpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) → ( ( 𝑋 = ∪ 𝑡 ∧ ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) ) )
103 102 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ( 𝑋 = ∪ 𝑡 ∧ ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑊 ∧ ∀ 𝑟 ∈ 𝑡 ( 𝑟 × { 𝐴 } ) ⊆ ( 𝑓 ‘ 𝑟 ) ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) ) )
104 51 103 mpd ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ∃ 𝑣 ∈ ( 𝒫 𝑊 ∩ Fin ) ( 𝑋 × 𝑢 ) ⊆ ∪ 𝑣 ) )