Metamath Proof Explorer

Theorem txtube

Description: The "tube lemma". If X is compact and there is an open set U containing the line X X. { A } , then there is a "tube" X X. u for some neighborhood u of A which is entirely contained within U . (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses txtube.x ⊢ 𝑋 = ∪ 𝑅
txtube.y ⊢ 𝑌 = ∪ 𝑆
txtube.r ⊢ ( 𝜑 → 𝑅 ∈ Comp )
txtube.s ⊢ ( 𝜑 → 𝑆 ∈ Top )
txtube.w ⊢ ( 𝜑 → 𝑈 ∈ ( 𝑅 ×t 𝑆 ) )
txtube.u ⊢ ( 𝜑 → ( 𝑋 × { 𝐴 } ) ⊆ 𝑈 )
txtube.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑌 )
Assertion txtube ( 𝜑 → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 txtube.x ⊢ 𝑋 = ∪ 𝑅
2 txtube.y ⊢ 𝑌 = ∪ 𝑆
3 txtube.r ⊢ ( 𝜑 → 𝑅 ∈ Comp )
4 txtube.s ⊢ ( 𝜑 → 𝑆 ∈ Top )
5 txtube.w ⊢ ( 𝜑 → 𝑈 ∈ ( 𝑅 ×t 𝑆 ) )
6 txtube.u ⊢ ( 𝜑 → ( 𝑋 × { 𝐴 } ) ⊆ 𝑈 )
7 txtube.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑌 )
8 eleq1 ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐴 ⟩ → ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ↔ ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ) )
9 8 anbi1d ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐴 ⟩ → ( ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
10 9 2rexbidv ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐴 ⟩ → ( ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
11 eltx ⊢ ( ( 𝑅 ∈ Comp ∧ 𝑆 ∈ Top ) → ( 𝑈 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
12 3 4 11 syl2anc ⊢ ( 𝜑 → ( 𝑈 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
13 5 12 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑈 ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) )
15 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 × { 𝐴 } ) ⊆ 𝑈 )
16 id ⊢ ( 𝑥 ∈ 𝑋 → 𝑥 ∈ 𝑋 )
17 snidg ⊢ ( 𝐴 ∈ 𝑌 → 𝐴 ∈ { 𝐴 } )
18 7 17 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
19 opelxpi ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ { 𝐴 } ) → ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑋 × { 𝐴 } ) )
20 16 18 19 syl2anr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑋 × { 𝐴 } ) )
21 15 20 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ⟨ 𝑥 , 𝐴 ⟩ ∈ 𝑈 )
22 10 14 21 rspcdva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) )
23 opelxp ⊢ ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ↔ ( 𝑥 ∈ 𝑢 ∧ 𝐴 ∈ 𝑣 ) )
24 23 anbi1i ⊢ ( ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ( ( 𝑥 ∈ 𝑢 ∧ 𝐴 ∈ 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) )
25 anass ⊢ ( ( ( 𝑥 ∈ 𝑢 ∧ 𝐴 ∈ 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ( 𝑥 ∈ 𝑢 ∧ ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
26 24 25 bitri ⊢ ( ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ( 𝑥 ∈ 𝑢 ∧ ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
27 26 rexbii ⊢ ( ∃ 𝑣 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ∃ 𝑣 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
28 r19.42v ⊢ ( ∃ 𝑣 ∈ 𝑆 ( 𝑥 ∈ 𝑢 ∧ ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) ↔ ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
29 27 28 bitri ⊢ ( ∃ 𝑣 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
30 29 rexbii ⊢ ( ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( ⟨ 𝑥 , 𝐴 ⟩ ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ∃ 𝑢 ∈ 𝑅 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
31 22 30 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑢 ∈ 𝑅 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
32 31 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑅 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) )
33 eleq2 ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝐴 ∈ 𝑣 ↔ 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ) )
34 xpeq2 ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝑢 × 𝑣 ) = ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) )
35 34 sseq1d ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( ( 𝑢 × 𝑣 ) ⊆ 𝑈 ↔ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) )
36 33 35 anbi12d ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ↔ ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) )
37 1 36 cmpcovf ⊢ ( ( 𝑅 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑢 ∈ 𝑅 ( 𝑥 ∈ 𝑢 ∧ ∃ 𝑣 ∈ 𝑆 ( 𝐴 ∈ 𝑣 ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑈 ) ) ) → ∃ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ( 𝑋 = ∪ 𝑡 ∧ ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) )
38 3 32 37 syl2anc ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ( 𝑋 = ∪ 𝑡 ∧ ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) )
39 rint0 ⊢ ( ran 𝑓 = ∅ → ( 𝑌 ∩ ∩ ran 𝑓 ) = 𝑌 )
40 39 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 = ∅ ) → ( 𝑌 ∩ ∩ ran 𝑓 ) = 𝑌 )
41 2 topopn ⊢ ( 𝑆 ∈ Top → 𝑌 ∈ 𝑆 )
42 4 41 syl ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
43 42 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 = ∅ ) → 𝑌 ∈ 𝑆 )
44 40 43 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 = ∅ ) → ( 𝑌 ∩ ∩ ran 𝑓 ) ∈ 𝑆 )
45 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → 𝑆 ∈ Top )
46 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝑓 : 𝑡 ⟶ 𝑆 )
47 46 frnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ran 𝑓 ⊆ 𝑆 )
48 47 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → ran 𝑓 ⊆ 𝑆 )
49 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → ran 𝑓 ≠ ∅ )
50 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) )
51 50 elin2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝑡 ∈ Fin )
52 46 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝑓 Fn 𝑡 )
53 dffn4 ⊢ ( 𝑓 Fn 𝑡 ↔ 𝑓 : 𝑡 –onto→ ran 𝑓 )
54 52 53 sylib ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝑓 : 𝑡 –onto→ ran 𝑓 )
55 fofi ⊢ ( ( 𝑡 ∈ Fin ∧ 𝑓 : 𝑡 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
56 51 54 55 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ran 𝑓 ∈ Fin )
57 56 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → ran 𝑓 ∈ Fin )
58 fiinopn ⊢ ( 𝑆 ∈ Top → ( ( ran 𝑓 ⊆ 𝑆 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin ) → ∩ ran 𝑓 ∈ 𝑆 ) )
59 58 imp ⊢ ( ( 𝑆 ∈ Top ∧ ( ran 𝑓 ⊆ 𝑆 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin ) ) → ∩ ran 𝑓 ∈ 𝑆 )
60 45 48 49 57 59 syl13anc ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → ∩ ran 𝑓 ∈ 𝑆 )
61 elssuni ⊢ ( ∩ ran 𝑓 ∈ 𝑆 → ∩ ran 𝑓 ⊆ ∪ 𝑆 )
62 60 61 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → ∩ ran 𝑓 ⊆ ∪ 𝑆 )
63 62 2 sseqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → ∩ ran 𝑓 ⊆ 𝑌 )
64 sseqin2 ⊢ ( ∩ ran 𝑓 ⊆ 𝑌 ↔ ( 𝑌 ∩ ∩ ran 𝑓 ) = ∩ ran 𝑓 )
65 63 64 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → ( 𝑌 ∩ ∩ ran 𝑓 ) = ∩ ran 𝑓 )
66 65 60 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) ∧ ran 𝑓 ≠ ∅ ) → ( 𝑌 ∩ ∩ ran 𝑓 ) ∈ 𝑆 )
67 44 66 pm2.61dane ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ( 𝑌 ∩ ∩ ran 𝑓 ) ∈ 𝑆 )
68 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝐴 ∈ 𝑌 )
69 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) )
70 simpl ⊢ ( ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) → 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) )
71 70 ralimi ⊢ ( ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) → ∀ 𝑢 ∈ 𝑡 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) )
72 69 71 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ∀ 𝑢 ∈ 𝑡 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) )
73 eliin ⊢ ( 𝐴 ∈ 𝑌 → ( 𝐴 ∈ ∩ 𝑢 ∈ 𝑡 ( 𝑓 ‘ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝑡 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ) )
74 68 73 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ( 𝐴 ∈ ∩ 𝑢 ∈ 𝑡 ( 𝑓 ‘ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝑡 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ) )
75 72 74 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝐴 ∈ ∩ 𝑢 ∈ 𝑡 ( 𝑓 ‘ 𝑢 ) )
76 fniinfv ⊢ ( 𝑓 Fn 𝑡 → ∩ 𝑢 ∈ 𝑡 ( 𝑓 ‘ 𝑢 ) = ∩ ran 𝑓 )
77 52 76 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ∩ 𝑢 ∈ 𝑡 ( 𝑓 ‘ 𝑢 ) = ∩ ran 𝑓 )
78 75 77 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝐴 ∈ ∩ ran 𝑓 )
79 68 78 elind ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝐴 ∈ ( 𝑌 ∩ ∩ ran 𝑓 ) )
80 simprl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝑋 = ∪ 𝑡 )
81 uniiun ⊢ ∪ 𝑡 = ∪ 𝑢 ∈ 𝑡 𝑢
82 80 81 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → 𝑋 = ∪ 𝑢 ∈ 𝑡 𝑢 )
83 82 xpeq1d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ( 𝑋 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) = ( ∪ 𝑢 ∈ 𝑡 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) )
84 xpiundir ⊢ ( ∪ 𝑢 ∈ 𝑡 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) = ∪ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) )
85 83 84 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ( 𝑋 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) = ∪ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) )
86 simpr ⊢ ( ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) → ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 )
87 86 ralimi ⊢ ( ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) → ∀ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 )
88 69 87 syl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ∀ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 )
89 inss2 ⊢ ( 𝑌 ∩ ∩ ran 𝑓 ) ⊆ ∩ ran 𝑓
90 76 adantr ⊢ ( ( 𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡 ) → ∩ 𝑢 ∈ 𝑡 ( 𝑓 ‘ 𝑢 ) = ∩ ran 𝑓 )
91 iinss2 ⊢ ( 𝑢 ∈ 𝑡 → ∩ 𝑢 ∈ 𝑡 ( 𝑓 ‘ 𝑢 ) ⊆ ( 𝑓 ‘ 𝑢 ) )
92 91 adantl ⊢ ( ( 𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡 ) → ∩ 𝑢 ∈ 𝑡 ( 𝑓 ‘ 𝑢 ) ⊆ ( 𝑓 ‘ 𝑢 ) )
93 90 92 eqsstrrd ⊢ ( ( 𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡 ) → ∩ ran 𝑓 ⊆ ( 𝑓 ‘ 𝑢 ) )
94 89 93 sstrid ⊢ ( ( 𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑌 ∩ ∩ ran 𝑓 ) ⊆ ( 𝑓 ‘ 𝑢 ) )
95 xpss2 ⊢ ( ( 𝑌 ∩ ∩ ran 𝑓 ) ⊆ ( 𝑓 ‘ 𝑢 ) → ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) )
96 sstr2 ⊢ ( ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) → ( ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 → ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 ) )
97 94 95 96 3syl ⊢ ( ( 𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡 ) → ( ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 → ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 ) )
98 97 ralimdva ⊢ ( 𝑓 Fn 𝑡 → ( ∀ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 → ∀ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 ) )
99 52 88 98 sylc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ∀ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 )
100 iunss ⊢ ( ∪ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 ↔ ∀ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 )
101 99 100 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ∪ 𝑢 ∈ 𝑡 ( 𝑢 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 )
102 85 101 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ( 𝑋 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 )
103 eleq2 ⊢ ( 𝑢 = ( 𝑌 ∩ ∩ ran 𝑓 ) → ( 𝐴 ∈ 𝑢 ↔ 𝐴 ∈ ( 𝑌 ∩ ∩ ran 𝑓 ) ) )
104 xpeq2 ⊢ ( 𝑢 = ( 𝑌 ∩ ∩ ran 𝑓 ) → ( 𝑋 × 𝑢 ) = ( 𝑋 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) )
105 104 sseq1d ⊢ ( 𝑢 = ( 𝑌 ∩ ∩ ran 𝑓 ) → ( ( 𝑋 × 𝑢 ) ⊆ 𝑈 ↔ ( 𝑋 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 ) )
106 103 105 anbi12d ⊢ ( 𝑢 = ( 𝑌 ∩ ∩ ran 𝑓 ) → ( ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) ↔ ( 𝐴 ∈ ( 𝑌 ∩ ∩ ran 𝑓 ) ∧ ( 𝑋 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 ) ) )
107 106 rspcev ⊢ ( ( ( 𝑌 ∩ ∩ ran 𝑓 ) ∈ 𝑆 ∧ ( 𝐴 ∈ ( 𝑌 ∩ ∩ ran 𝑓 ) ∧ ( 𝑋 × ( 𝑌 ∩ ∩ ran 𝑓 ) ) ⊆ 𝑈 ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) )
108 67 79 102 107 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ ( 𝑋 = ∪ 𝑡 ∧ ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) )
109 108 expr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ 𝑋 = ∪ 𝑡 ) → ( ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) ) )
110 109 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) ∧ 𝑋 = ∪ 𝑡 ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) ) )
111 110 expimpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ) → ( ( 𝑋 = ∪ 𝑡 ∧ ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) ) )
112 111 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( 𝒫 𝑅 ∩ Fin ) ( 𝑋 = ∪ 𝑡 ∧ ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑆 ∧ ∀ 𝑢 ∈ 𝑡 ( 𝐴 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑢 × ( 𝑓 ‘ 𝑢 ) ) ⊆ 𝑈 ) ) ) → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) ) )
113 38 112 mpd ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑆 ( 𝐴 ∈ 𝑢 ∧ ( 𝑋 × 𝑢 ) ⊆ 𝑈 ) )