MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptcnplem Structured version   Visualization version   GIF version

Theorem ptcnplem 23125
Description: Lemma for ptcnp 23126. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
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
Ref Expression
ptcnplem ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
Distinct variable groups:   𝑧,𝐴   π‘₯,π‘˜,𝑧,𝐷   π‘˜,𝐼,π‘₯,𝑧   π‘₯,𝐺,𝑧   π‘˜,𝐽,𝑧   𝑧,𝐾   πœ‘,π‘˜,π‘₯,𝑧   π‘˜,𝐹,π‘₯,𝑧   π‘˜,𝑉,π‘₯   π‘˜,π‘Š,𝑧   π‘˜,𝑋,π‘₯,𝑧
Allowed substitution hints:   πœ“(π‘₯,𝑧,π‘˜)   𝐴(π‘₯,π‘˜)   𝐺(π‘˜)   𝐽(π‘₯)   𝐾(π‘₯,π‘˜)   𝑉(𝑧)   π‘Š(π‘₯)

Proof of Theorem ptcnplem
Dummy variables 𝑓 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcnplem.4 . . . 4 ((πœ‘ ∧ πœ“) β†’ π‘Š ∈ Fin)
2 inss2 4230 . . . 4 (𝐼 ∩ π‘Š) βŠ† π‘Š
3 ssfi 9173 . . . 4 ((π‘Š ∈ Fin ∧ (𝐼 ∩ π‘Š) βŠ† π‘Š) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
41, 2, 3sylancl 587 . . 3 ((πœ‘ ∧ πœ“) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
5 nfv 1918 . . . . 5 β„²π‘˜πœ‘
6 ptcnplem.1 . . . . 5 β„²π‘˜πœ“
75, 6nfan 1903 . . . 4 β„²π‘˜(πœ‘ ∧ πœ“)
8 elinel1 4196 . . . . . 6 (π‘˜ ∈ (𝐼 ∩ π‘Š) β†’ π‘˜ ∈ 𝐼)
9 ptcnp.7 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·))
109adantlr 714 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·))
11 ptcnplem.3 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ (πΊβ€˜π‘˜) ∈ (πΉβ€˜π‘˜))
12 ptcnp.6 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐷 ∈ 𝑋)
1312adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ 𝐷 ∈ 𝑋)
14 simpr 486 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
15 ptcnp.3 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
1615adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
17 ptcnp.5 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐹:𝐼⟢Top)
1817ffvelcdmda 7087 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ Top)
19 toptopon2 22420 . . . . . . . . . . . . . . . . . . . . 21 ((πΉβ€˜π‘˜) ∈ Top ↔ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
2018, 19sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
21 cnpf2 22754 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
2216, 20, 9, 21syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
23 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ 𝑋 ↦ 𝐴) = (π‘₯ ∈ 𝑋 ↦ 𝐴)
2423fmpt 7110 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ↔ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
2522, 24sylibr 233 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
2625r19.21bi 3249 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
2723fvmpt2 7010 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ 𝑋 ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
2814, 26, 27syl2anc 585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
2928an32s 651 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ 𝐼) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
3029mpteq2dva 5249 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
31 simpr 486 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
32 ptcnp.4 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐼 ∈ 𝑉)
3332adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐼 ∈ 𝑉)
3433mptexd 7226 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
35 eqid 2733 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
3635fvmpt2 7010 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝑋 ∧ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
3731, 34, 36syl2anc 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
3830, 37eqtr4d 2776 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
3938ralrimiva 3147 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
4039adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
41 nfcv 2904 . . . . . . . . . . . . . 14 β„²π‘₯𝐼
42 nffvmpt1 6903 . . . . . . . . . . . . . 14 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)
4341, 42nfmpt 5256 . . . . . . . . . . . . 13 β„²π‘₯(π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·))
44 nffvmpt1 6903 . . . . . . . . . . . . 13 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
4543, 44nfeq 2917 . . . . . . . . . . . 12 β„²π‘₯(π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
46 fveq2 6892 . . . . . . . . . . . . . 14 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·))
4746mpteq2dv 5251 . . . . . . . . . . . . 13 (π‘₯ = 𝐷 β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)))
48 fveq2 6892 . . . . . . . . . . . . 13 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·))
4947, 48eqeq12d 2749 . . . . . . . . . . . 12 (π‘₯ = 𝐷 β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ↔ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)))
5045, 49rspc 3601 . . . . . . . . . . 11 (𝐷 ∈ 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)))
5113, 40, 50sylc 65 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·))
52 ptcnplem.6 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
5351, 52eqeltrd 2834 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
5432adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ 𝐼 ∈ 𝑉)
55 mptelixpg 8929 . . . . . . . . . 10 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)))
5654, 55syl 17 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)))
5753, 56mpbid 231 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜))
5857r19.21bi 3249 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜))
59 cnpimaex 22760 . . . . . . 7 (((π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·) ∧ (πΊβ€˜π‘˜) ∈ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
6010, 11, 58, 59syl3anc 1372 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
618, 60sylan2 594 . . . . 5 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
6261ex 414 . . . 4 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ (𝐼 ∩ π‘Š) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜))))
637, 62ralrimi 3255 . . 3 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
64 eleq2 2823 . . . . 5 (𝑒 = (π‘“β€˜π‘˜) β†’ (𝐷 ∈ 𝑒 ↔ 𝐷 ∈ (π‘“β€˜π‘˜)))
65 imaeq2 6056 . . . . . 6 (𝑒 = (π‘“β€˜π‘˜) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) = ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)))
6665sseq1d 4014 . . . . 5 (𝑒 = (π‘“β€˜π‘˜) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))
6764, 66anbi12d 632 . . . 4 (𝑒 = (π‘“β€˜π‘˜) β†’ ((𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)) ↔ (𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
6867ac6sfi 9287 . . 3 (((𝐼 ∩ π‘Š) ∈ Fin ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜))) β†’ βˆƒπ‘“(𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
694, 63, 68syl2anc 585 . 2 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘“(𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
7015ad2antrr 725 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
71 toponuni 22416 . . . . . 6 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
7270, 71syl 17 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑋 = βˆͺ 𝐽)
7372ineq1d 4212 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) = (βˆͺ 𝐽 ∩ ∩ ran 𝑓))
74 topontop 22415 . . . . . . 7 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
7515, 74syl 17 . . . . . 6 (πœ‘ β†’ 𝐽 ∈ Top)
7675ad2antrr 725 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐽 ∈ Top)
77 frn 6725 . . . . . 6 (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 β†’ ran 𝑓 βŠ† 𝐽)
7877ad2antrl 727 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ ran 𝑓 βŠ† 𝐽)
794adantr 482 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
80 ffn 6718 . . . . . . . 8 (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
8180ad2antrl 727 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
82 dffn4 6812 . . . . . . 7 (𝑓 Fn (𝐼 ∩ π‘Š) ↔ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓)
8381, 82sylib 217 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓)
84 fofi 9338 . . . . . 6 (((𝐼 ∩ π‘Š) ∈ Fin ∧ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
8579, 83, 84syl2anc 585 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ ran 𝑓 ∈ Fin)
86 eqid 2733 . . . . . 6 βˆͺ 𝐽 = βˆͺ 𝐽
8786rintopn 22411 . . . . 5 ((𝐽 ∈ Top ∧ ran 𝑓 βŠ† 𝐽 ∧ ran 𝑓 ∈ Fin) β†’ (βˆͺ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
8876, 78, 85, 87syl3anc 1372 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (βˆͺ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
8973, 88eqeltrd 2834 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽)
9012ad2antrr 725 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐷 ∈ 𝑋)
91 simpl 484 . . . . . . 7 ((𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ 𝐷 ∈ (π‘“β€˜π‘˜))
9291ralimi 3084 . . . . . 6 (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜))
9392ad2antll 728 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜))
94 eleq2 2823 . . . . . . 7 (𝑧 = (π‘“β€˜π‘˜) β†’ (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (π‘“β€˜π‘˜)))
9594ralrn 7090 . . . . . 6 (𝑓 Fn (𝐼 ∩ π‘Š) β†’ (βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜)))
9681, 95syl 17 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜)))
9793, 96mpbird 257 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧)
98 elrint 4996 . . . 4 (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ↔ (𝐷 ∈ 𝑋 ∧ βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧))
9990, 97, 98sylanbrc 584 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓))
100 nfv 1918 . . . . . . . . . 10 β„²π‘˜ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽
1017, 100nfan 1903 . . . . . . . . 9 β„²π‘˜((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽)
102 funmpt 6587 . . . . . . . . . . . . 13 Fun (π‘₯ ∈ 𝑋 ↦ 𝐴)
103 simp-4l 782 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ πœ‘)
104103, 15syl 17 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
105 simpllr 775 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽)
106 simplr 768 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ π‘˜ ∈ (𝐼 ∩ π‘Š))
107105, 106ffvelcdmd 7088 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) ∈ 𝐽)
108 toponss 22429 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘“β€˜π‘˜) ∈ 𝐽) β†’ (π‘“β€˜π‘˜) βŠ† 𝑋)
109104, 107, 108syl2anc 585 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) βŠ† 𝑋)
110106elin1d 4199 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ π‘˜ ∈ 𝐼)
111103, 110, 25syl2anc 585 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
112 dmmptg 6242 . . . . . . . . . . . . . . 15 (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐴) = 𝑋)
113111, 112syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐴) = 𝑋)
114109, 113sseqtrrd 4024 . . . . . . . . . . . . 13 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐴))
115 funimass4 6957 . . . . . . . . . . . . 13 ((Fun (π‘₯ ∈ 𝑋 ↦ 𝐴) ∧ (π‘“β€˜π‘˜) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐴)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)))
116102, 114, 115sylancr 588 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)))
117 nffvmpt1 6903 . . . . . . . . . . . . . 14 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘)
118117nfel1 2920 . . . . . . . . . . . . 13 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)
119 nfv 1918 . . . . . . . . . . . . 13 Ⅎ𝑑((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)
120 fveq2 6892 . . . . . . . . . . . . . 14 (𝑑 = π‘₯ β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯))
121120eleq1d 2819 . . . . . . . . . . . . 13 (𝑑 = π‘₯ β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
122118, 119, 121cbvralw 3304 . . . . . . . . . . . 12 (βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜))
123116, 122bitrdi 287 . . . . . . . . . . 11 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
124 inss1 4229 . . . . . . . . . . . . 13 (𝑋 ∩ ∩ ran 𝑓) βŠ† 𝑋
125 ssralv 4051 . . . . . . . . . . . . 13 ((𝑋 ∩ ∩ ran 𝑓) βŠ† 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
126124, 111, 125mpsyl 68 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
127 inss2 4230 . . . . . . . . . . . . . 14 (𝑋 ∩ ∩ ran 𝑓) βŠ† ∩ ran 𝑓
128105, 80syl 17 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
129 fnfvelrn 7083 . . . . . . . . . . . . . . . 16 ((𝑓 Fn (𝐼 ∩ π‘Š) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) β†’ (π‘“β€˜π‘˜) ∈ ran 𝑓)
130128, 106, 129syl2anc 585 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) ∈ ran 𝑓)
131 intss1 4968 . . . . . . . . . . . . . . 15 ((π‘“β€˜π‘˜) ∈ ran 𝑓 β†’ ∩ ran 𝑓 βŠ† (π‘“β€˜π‘˜))
132130, 131syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ ∩ ran 𝑓 βŠ† (π‘“β€˜π‘˜))
133127, 132sstrid 3994 . . . . . . . . . . . . 13 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (𝑋 ∩ ∩ ran 𝑓) βŠ† (π‘“β€˜π‘˜))
134 ssralv 4051 . . . . . . . . . . . . 13 ((𝑋 ∩ ∩ ran 𝑓) βŠ† (π‘“β€˜π‘˜) β†’ (βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
135133, 134syl 17 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
136 r19.26 3112 . . . . . . . . . . . . 13 (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) ↔ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
137 elinel1 4196 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) β†’ π‘₯ ∈ 𝑋)
138137, 27sylan 581 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
139138eleq1d 2819 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) ↔ 𝐴 ∈ (πΊβ€˜π‘˜)))
140139biimpd 228 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ 𝐴 ∈ (πΊβ€˜π‘˜)))
141140expimpd 455 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) β†’ ((𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) β†’ 𝐴 ∈ (πΊβ€˜π‘˜)))
142141ralimia 3081 . . . . . . . . . . . . 13 (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
143136, 142sylbir 234 . . . . . . . . . . . 12 ((βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
144126, 135, 143syl6an 683 . . . . . . . . . . 11 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
145123, 144sylbid 239 . . . . . . . . . 10 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
146145expimpd 455 . . . . . . . . 9 ((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) β†’ ((𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
147101, 146ralimdaa 3258 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) β†’ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
148147impr 456 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
149 simpl 484 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ πœ‘)
150 eldifi 4127 . . . . . . . . . . . 12 (π‘˜ ∈ (𝐼 βˆ– π‘Š) β†’ π‘˜ ∈ 𝐼)
151137, 26sylan2 594 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
152151ralrimiva 3147 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
153149, 150, 152syl2an 597 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
154 ptcnplem.5 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ (πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
155 eleq2 2823 . . . . . . . . . . . . 13 ((πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜) β†’ (𝐴 ∈ (πΊβ€˜π‘˜) ↔ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
156155ralbidv 3178 . . . . . . . . . . . 12 ((πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜) β†’ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
157154, 156syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
158153, 157mpbird 257 . . . . . . . . . 10 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
159158ex 414 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ (𝐼 βˆ– π‘Š) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
1607, 159ralrimi 3255 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
161160adantr 482 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
162 inundif 4479 . . . . . . . . 9 ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š)) = 𝐼
163162raleqi 3324 . . . . . . . 8 (βˆ€π‘˜ ∈ ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š))βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
164 ralunb 4192 . . . . . . . 8 (βˆ€π‘˜ ∈ ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š))βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ∧ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
165163, 164bitr3i 277 . . . . . . 7 (βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ∧ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
166148, 161, 165sylanbrc 584 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
167 ralcom 3287 . . . . . 6 (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
168166, 167sylibr 233 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜))
16932ad2antrr 725 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐼 ∈ 𝑉)
170 nffvmpt1 6903 . . . . . . . . 9 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘)
171170nfel1 2920 . . . . . . . 8 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)
172 nfv 1918 . . . . . . . 8 Ⅎ𝑑((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)
173 fveq2 6892 . . . . . . . . 9 (𝑑 = π‘₯ β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
174173eleq1d 2819 . . . . . . . 8 (𝑑 = π‘₯ β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
175171, 172, 174cbvralw 3304 . . . . . . 7 (βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
176 mptexg 7223 . . . . . . . . . . 11 (𝐼 ∈ 𝑉 β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
177137, 176, 36syl2anr 598 . . . . . . . . . 10 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
178177eleq1d 2819 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
179 mptelixpg 8929 . . . . . . . . . 10 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
180179adantr 482 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
181178, 180bitrd 279 . . . . . . . 8 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
182181ralbidva 3176 . . . . . . 7 (𝐼 ∈ 𝑉 β†’ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
183175, 182bitrid 283 . . . . . 6 (𝐼 ∈ 𝑉 β†’ (βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
184169, 183syl 17 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
185168, 184mpbird 257 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
186 funmpt 6587 . . . . 5 Fun (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
18732mptexd 7226 . . . . . . . . 9 (πœ‘ β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
188187ralrimivw 3151 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
189188ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
190 dmmptg 6242 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V β†’ dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = 𝑋)
191189, 190syl 17 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = 𝑋)
192124, 191sseqtrrid 4036 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) βŠ† dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)))
193 funimass4 6957 . . . . 5 ((Fun (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) ∧ (𝑋 ∩ ∩ ran 𝑓) βŠ† dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
194186, 192, 193sylancr 588 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
195185, 194mpbird 257 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
196 eleq2 2823 . . . . 5 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓)))
197 imaeq2 6056 . . . . . 6 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)))
198197sseq1d 4014 . . . . 5 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
199196, 198anbi12d 632 . . . 4 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)) ↔ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))))
200199rspcev 3613 . . 3 (((𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
20189, 99, 195, 200syl12anc 836 . 2 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
20269, 201exlimddv 1939 1 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  βˆƒwex 1782  β„²wnf 1786   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆ– cdif 3946   βˆͺ cun 3947   ∩ cin 3948   βŠ† wss 3949  βˆͺ cuni 4909  βˆ© cint 4951   ↦ cmpt 5232  dom cdm 5677  ran crn 5678   β€œ cima 5680  Fun wfun 6538   Fn wfn 6539  βŸΆwf 6540  β€“ontoβ†’wfo 6542  β€˜cfv 6544  (class class class)co 7409  Xcixp 8891  Fincfn 8939  βˆtcpt 17384  Topctop 22395  TopOnctopon 22412   CnP ccnp 22729
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-dom 8941  df-fin 8943  df-top 22396  df-topon 22413  df-cnp 22732
This theorem is referenced by:  ptcnp  23126
  Copyright terms: Public domain W3C validator