Metamath Proof Explorer

Theorem ptcnplem

Description: Lemma for ptcnp . (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses ptcnp.2 ⊢ 𝐾 = ( ∏t ‘ 𝐹 )
ptcnp.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
ptcnp.4 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
ptcnp.5 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ Top )
ptcnp.6 ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 )
ptcnp.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝐷 ) )
ptcnplem.1 ⊢ Ⅎ 𝑘 𝜓
ptcnplem.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 Fn 𝐼 )
ptcnplem.3 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
ptcnplem.4 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ Fin )
ptcnplem.5 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ) → ( 𝐺 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
ptcnplem.6 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) )
Assertion ptcnplem ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 ptcnp.2 ⊢ 𝐾 = ( ∏t ‘ 𝐹 )
2 ptcnp.3 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 ptcnp.4 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 ptcnp.5 ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ Top )
5 ptcnp.6 ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 )
6 ptcnp.7 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝐷 ) )
7 ptcnplem.1 ⊢ Ⅎ 𝑘 𝜓
8 ptcnplem.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 Fn 𝐼 )
9 ptcnplem.3 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) )
10 ptcnplem.4 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ∈ Fin )
11 ptcnplem.5 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ) → ( 𝐺 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
12 ptcnplem.6 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) )
13 inss2 ⊢ ( 𝐼 ∩ 𝑊 ) ⊆ 𝑊
14 ssfi ⊢ ( ( 𝑊 ∈ Fin ∧ ( 𝐼 ∩ 𝑊 ) ⊆ 𝑊 ) → ( 𝐼 ∩ 𝑊 ) ∈ Fin )
15 10 13 14 sylancl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐼 ∩ 𝑊 ) ∈ Fin )
16 nfv ⊢ Ⅎ 𝑘 𝜑
17 16 7 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝜓 )
18 elinel1 ⊢ ( 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) → 𝑘 ∈ 𝐼 )
19 6 adantlr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝐷 ) )
20 5 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐷 ∈ 𝑋 )
21 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
22 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
23 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ Top )
24 toptopon2 ⊢ ( ( 𝐹 ‘ 𝑘 ) ∈ Top ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
25 23 24 sylib ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) )
26 cnpf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( TopOn ‘ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝐷 ) ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
27 22 25 6 26 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
28 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
29 28 fmpt ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ∪ ( 𝐹 ‘ 𝑘 ) )
30 27 29 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
31 30 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
32 28 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
33 21 31 32 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
34 33 an32s ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
35 34 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
37 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐼 ∈ 𝑉 )
38 37 mptexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ V )
39 eqid ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) )
40 39 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ V ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) )
41 36 38 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) )
42 35 41 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) )
43 42 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) )
45 nfcv ⊢ Ⅎ 𝑥 𝐼
46 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 )
47 45 46 nfmpt ⊢ Ⅎ 𝑥 ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) )
48 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 )
49 47 48 nfeq ⊢ Ⅎ 𝑥 ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 )
50 fveq2 ⊢ ( 𝑥 = 𝐷 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) )
51 50 mpteq2dv ⊢ ( 𝑥 = 𝐷 → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ) )
52 fveq2 ⊢ ( 𝑥 = 𝐷 → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) )
53 51 52 eqeq12d ⊢ ( 𝑥 = 𝐷 → ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) ↔ ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ) )
54 49 53 rspc ⊢ ( 𝐷 ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) ) )
55 20 44 54 sylc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝐷 ) )
56 55 12 eqeltrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) )
57 3 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐼 ∈ 𝑉 )
58 mptelixpg ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
59 57 58 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
60 56 59 mpbid ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑘 ∈ 𝐼 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ ( 𝐺 ‘ 𝑘 ) )
61 60 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ ( 𝐺 ‘ 𝑘 ) )
62 cnpimaex ⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( ( 𝐽 CnP ( 𝐹 ‘ 𝑘 ) ) ‘ 𝐷 ) ∧ ( 𝐺 ‘ 𝑘 ) ∈ ( 𝐹 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝐷 ) ∈ ( 𝐺 ‘ 𝑘 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝐷 ∈ 𝑢 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) ⊆ ( 𝐺 ‘ 𝑘 ) ) )
63 19 9 61 62 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ 𝐼 ) → ∃ 𝑢 ∈ 𝐽 ( 𝐷 ∈ 𝑢 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) ⊆ ( 𝐺 ‘ 𝑘 ) ) )
64 18 63 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝐷 ∈ 𝑢 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) ⊆ ( 𝐺 ‘ 𝑘 ) ) )
65 64 ex ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) → ∃ 𝑢 ∈ 𝐽 ( 𝐷 ∈ 𝑢 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) )
66 17 65 ralrimi ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ∃ 𝑢 ∈ 𝐽 ( 𝐷 ∈ 𝑢 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) ⊆ ( 𝐺 ‘ 𝑘 ) ) )
67 eleq2 ⊢ ( 𝑢 = ( 𝑓 ‘ 𝑘 ) → ( 𝐷 ∈ 𝑢 ↔ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) )
68 imaeq2 ⊢ ( 𝑢 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) )
69 68 sseq1d ⊢ ( 𝑢 = ( 𝑓 ‘ 𝑘 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) ⊆ ( 𝐺 ‘ 𝑘 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) )
70 67 69 anbi12d ⊢ ( 𝑢 = ( 𝑓 ‘ 𝑘 ) → ( ( 𝐷 ∈ 𝑢 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) )
71 70 ac6sfi ⊢ ( ( ( 𝐼 ∩ 𝑊 ) ∈ Fin ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ∃ 𝑢 ∈ 𝐽 ( 𝐷 ∈ 𝑢 ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ 𝑢 ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) → ∃ 𝑓 ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) )
72 15 66 71 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑓 ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) )
73 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
74 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
75 73 74 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → 𝑋 = ∪ 𝐽 )
76 75 ineq1d ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( 𝑋 ∩ ∩ ran 𝑓 ) = ( ∪ 𝐽 ∩ ∩ ran 𝑓 ) )
77 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
78 2 77 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
79 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → 𝐽 ∈ Top )
80 frn ⊢ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 → ran 𝑓 ⊆ 𝐽 )
81 80 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ran 𝑓 ⊆ 𝐽 )
82 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( 𝐼 ∩ 𝑊 ) ∈ Fin )
83 ffn ⊢ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 → 𝑓 Fn ( 𝐼 ∩ 𝑊 ) )
84 83 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → 𝑓 Fn ( 𝐼 ∩ 𝑊 ) )
85 dffn4 ⊢ ( 𝑓 Fn ( 𝐼 ∩ 𝑊 ) ↔ 𝑓 : ( 𝐼 ∩ 𝑊 ) –onto→ ran 𝑓 )
86 84 85 sylib ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → 𝑓 : ( 𝐼 ∩ 𝑊 ) –onto→ ran 𝑓 )
87 fofi ⊢ ( ( ( 𝐼 ∩ 𝑊 ) ∈ Fin ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
88 82 86 87 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ran 𝑓 ∈ Fin )
89 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
90 89 rintopn ⊢ ( ( 𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ∈ Fin ) → ( ∪ 𝐽 ∩ ∩ ran 𝑓 ) ∈ 𝐽 )
91 79 81 88 90 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( ∪ 𝐽 ∩ ∩ ran 𝑓 ) ∈ 𝐽 )
92 76 91 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( 𝑋 ∩ ∩ ran 𝑓 ) ∈ 𝐽 )
93 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → 𝐷 ∈ 𝑋 )
94 simpl ⊢ ( ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) → 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) )
95 94 ralimi ⊢ ( ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) )
96 95 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) )
97 eleq2 ⊢ ( 𝑧 = ( 𝑓 ‘ 𝑘 ) → ( 𝐷 ∈ 𝑧 ↔ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) )
98 97 ralrn ⊢ ( 𝑓 Fn ( 𝐼 ∩ 𝑊 ) → ( ∀ 𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) )
99 84 98 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( ∀ 𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) )
100 96 99 mpbird ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∀ 𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 )
101 elrint ⊢ ( 𝐷 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ↔ ( 𝐷 ∈ 𝑋 ∧ ∀ 𝑧 ∈ ran 𝑓 𝐷 ∈ 𝑧 ) )
102 93 100 101 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → 𝐷 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) )
103 nfv ⊢ Ⅎ 𝑘 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽
104 17 103 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 )
105 funmpt ⊢ Fun ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
106 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → 𝜑 )
107 106 2 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
108 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 )
109 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) )
110 108 109 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝐽 )
111 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑓 ‘ 𝑘 ) ∈ 𝐽 ) → ( 𝑓 ‘ 𝑘 ) ⊆ 𝑋 )
112 107 110 111 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( 𝑓 ‘ 𝑘 ) ⊆ 𝑋 )
113 109 elin1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → 𝑘 ∈ 𝐼 )
114 106 113 30 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
115 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) → dom ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = 𝑋 )
116 114 115 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → dom ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) = 𝑋 )
117 112 116 sseqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( 𝑓 ‘ 𝑘 ) ⊆ dom ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
118 funimass4 ⊢ ( ( Fun ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∧ ( 𝑓 ‘ 𝑘 ) ⊆ dom ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑡 ∈ ( 𝑓 ‘ 𝑘 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
119 105 117 118 sylancr ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑡 ∈ ( 𝑓 ‘ 𝑘 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
120 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 )
121 120 nfel1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) ∈ ( 𝐺 ‘ 𝑘 )
122 nfv ⊢ Ⅎ 𝑡 ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 )
123 fveq2 ⊢ ( 𝑡 = 𝑥 → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) = ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) )
124 123 eleq1d ⊢ ( 𝑡 = 𝑥 → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) ∈ ( 𝐺 ‘ 𝑘 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
125 121 122 124 cbvralw ⊢ ( ∀ 𝑡 ∈ ( 𝑓 ‘ 𝑘 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑡 ) ∈ ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ( 𝑓 ‘ 𝑘 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) )
126 119 125 bitrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ( 𝑓 ‘ 𝑘 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
127 inss1 ⊢ ( 𝑋 ∩ ∩ ran 𝑓 ) ⊆ 𝑋
128 ssralv ⊢ ( ( 𝑋 ∩ ∩ ran 𝑓 ) ⊆ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
129 127 114 128 mpsyl ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
130 inss2 ⊢ ( 𝑋 ∩ ∩ ran 𝑓 ) ⊆ ∩ ran 𝑓
131 108 83 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → 𝑓 Fn ( 𝐼 ∩ 𝑊 ) )
132 fnfvelrn ⊢ ( ( 𝑓 Fn ( 𝐼 ∩ 𝑊 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ran 𝑓 )
133 131 109 132 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ran 𝑓 )
134 intss1 ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ ran 𝑓 → ∩ ran 𝑓 ⊆ ( 𝑓 ‘ 𝑘 ) )
135 133 134 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ∩ ran 𝑓 ⊆ ( 𝑓 ‘ 𝑘 ) )
136 130 135 sstrid ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( 𝑋 ∩ ∩ ran 𝑓 ) ⊆ ( 𝑓 ‘ 𝑘 ) )
137 ssralv ⊢ ( ( 𝑋 ∩ ∩ ran 𝑓 ) ⊆ ( 𝑓 ‘ 𝑘 ) → ( ∀ 𝑥 ∈ ( 𝑓 ‘ 𝑘 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
138 136 137 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( ∀ 𝑥 ∈ ( 𝑓 ‘ 𝑘 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
139 r19.26 ⊢ ( ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) ↔ ( ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) )
140 elinel1 ⊢ ( 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) → 𝑥 ∈ 𝑋 )
141 140 32 sylan ⊢ ( ( 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∧ 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
142 141 eleq1d ⊢ ( ( 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∧ 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ↔ 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
143 142 biimpd ⊢ ( ( 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∧ 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) → 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
144 143 expimpd ⊢ ( 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) → ( ( 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) → 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
145 144 ralimia ⊢ ( ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
146 139 145 sylbir ⊢ ( ( ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ∧ ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
147 129 138 146 syl6an ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( ∀ 𝑥 ∈ ( 𝑓 ‘ 𝑘 ) ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ‘ 𝑥 ) ∈ ( 𝐺 ‘ 𝑘 ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
148 126 147 sylbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) ∧ 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
149 148 expimpd ⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) ∧ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ) → ( ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
150 104 149 ralimdaa ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ) → ( ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
151 150 impr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
152 simpl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
153 eldifi ⊢ ( 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) → 𝑘 ∈ 𝐼 )
154 140 31 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ) → 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
155 154 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
156 152 153 155 syl2an ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
157 eleq2 ⊢ ( ( 𝐺 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) → ( 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ↔ 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
158 157 ralbidv ⊢ ( ( 𝐺 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 ) → ( ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
159 11 158 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ) → ( ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
160 156 159 mpbird ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
161 160 ex ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
162 17 161 ralrimi ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
163 162 adantr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
164 inundif ⊢ ( ( 𝐼 ∩ 𝑊 ) ∪ ( 𝐼 ∖ 𝑊 ) ) = 𝐼
165 164 raleqi ⊢ ( ∀ 𝑘 ∈ ( ( 𝐼 ∩ 𝑊 ) ∪ ( 𝐼 ∖ 𝑊 ) ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
166 ralunb ⊢ ( ∀ 𝑘 ∈ ( ( 𝐼 ∩ 𝑊 ) ∪ ( 𝐼 ∖ 𝑊 ) ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ↔ ( ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
167 165 166 bitr3i ⊢ ( ∀ 𝑘 ∈ 𝐼 ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ↔ ( ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ∧ ∀ 𝑘 ∈ ( 𝐼 ∖ 𝑊 ) ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
168 151 163 167 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∀ 𝑘 ∈ 𝐼 ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
169 ralcom ⊢ ( ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
170 168 169 sylibr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) )
171 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → 𝐼 ∈ 𝑉 )
172 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 )
173 172 nfel1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 )
174 nfv ⊢ Ⅎ 𝑡 ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 )
175 fveq2 ⊢ ( 𝑡 = 𝑥 → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) )
176 175 eleq1d ⊢ ( 𝑡 = 𝑥 → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )
177 173 174 176 cbvralw ⊢ ( ∀ 𝑡 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) )
178 mptexg ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ V )
179 140 178 40 syl2anr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) = ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) )
180 179 eleq1d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )
181 mptelixpg ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
182 181 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ) → ( ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
183 180 182 bitrd ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
184 183 ralbidva ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑥 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
185 177 184 bitrid ⊢ ( 𝐼 ∈ 𝑉 → ( ∀ 𝑡 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
186 171 185 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( ∀ 𝑡 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑥 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∀ 𝑘 ∈ 𝐼 𝐴 ∈ ( 𝐺 ‘ 𝑘 ) ) )
187 170 186 mpbird ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∀ 𝑡 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) )
188 funmpt ⊢ Fun ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) )
189 3 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ V )
190 189 ralrimivw ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ V )
191 190 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ V )
192 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ∈ V → dom ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) = 𝑋 )
193 191 192 syl ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → dom ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) = 𝑋 )
194 127 193 sseqtrrid ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( 𝑋 ∩ ∩ ran 𝑓 ) ⊆ dom ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) )
195 funimass4 ⊢ ( ( Fun ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ∧ ( 𝑋 ∩ ∩ ran 𝑓 ) ⊆ dom ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ ( 𝑋 ∩ ∩ ran 𝑓 ) ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑡 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )
196 188 194 195 sylancr ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ ( 𝑋 ∩ ∩ ran 𝑓 ) ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ∀ 𝑡 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) ‘ 𝑡 ) ∈ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )
197 187 196 mpbird ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ ( 𝑋 ∩ ∩ ran 𝑓 ) ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) )
198 eleq2 ⊢ ( 𝑧 = ( 𝑋 ∩ ∩ ran 𝑓 ) → ( 𝐷 ∈ 𝑧 ↔ 𝐷 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ) )
199 imaeq2 ⊢ ( 𝑧 = ( 𝑋 ∩ ∩ ran 𝑓 ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) = ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ ( 𝑋 ∩ ∩ ran 𝑓 ) ) )
200 199 sseq1d ⊢ ( 𝑧 = ( 𝑋 ∩ ∩ ran 𝑓 ) → ( ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ↔ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ ( 𝑋 ∩ ∩ ran 𝑓 ) ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )
201 198 200 anbi12d ⊢ ( 𝑧 = ( 𝑋 ∩ ∩ ran 𝑓 ) → ( ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) ↔ ( 𝐷 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ ( 𝑋 ∩ ∩ ran 𝑓 ) ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) ) )
202 201 rspcev ⊢ ( ( ( 𝑋 ∩ ∩ ran 𝑓 ) ∈ 𝐽 ∧ ( 𝐷 ∈ ( 𝑋 ∩ ∩ ran 𝑓 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ ( 𝑋 ∩ ∩ ran 𝑓 ) ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )
203 92 102 197 202 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑓 : ( 𝐼 ∩ 𝑊 ) ⟶ 𝐽 ∧ ∀ 𝑘 ∈ ( 𝐼 ∩ 𝑊 ) ( 𝐷 ∈ ( 𝑓 ‘ 𝑘 ) ∧ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) “ ( 𝑓 ‘ 𝑘 ) ) ⊆ ( 𝐺 ‘ 𝑘 ) ) ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )
204 72 203 exlimddv ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∃ 𝑧 ∈ 𝐽 ( 𝐷 ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑘 ∈ 𝐼 ↦ 𝐴 ) ) “ 𝑧 ) ⊆ X 𝑘 ∈ 𝐼 ( 𝐺 ‘ 𝑘 ) ) )