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

Theorem ptcnplem 22988
Description: Lemma for ptcnp 22989. (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 4194 . . . 4 (𝐼 ∩ π‘Š) βŠ† π‘Š
3 ssfi 9124 . . . 4 ((π‘Š ∈ Fin ∧ (𝐼 ∩ π‘Š) βŠ† π‘Š) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
41, 2, 3sylancl 587 . . 3 ((πœ‘ ∧ πœ“) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
5 nfv 1918 . . . . 5 β„²π‘˜πœ‘
6 ptcnplem.1 . . . . 5 β„²π‘˜πœ“
75, 6nfan 1903 . . . 4 β„²π‘˜(πœ‘ ∧ πœ“)
8 elinel1 4160 . . . . . 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 7040 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ Top)
19 toptopon2 22283 . . . . . . . . . . . . . . . . . . . . 21 ((πΉβ€˜π‘˜) ∈ Top ↔ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
2018, 19sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
21 cnpf2 22617 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
2216, 20, 9, 21syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
23 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ 𝑋 ↦ 𝐴) = (π‘₯ ∈ 𝑋 ↦ 𝐴)
2423fmpt 7063 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ↔ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
2522, 24sylibr 233 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
2625r19.21bi 3237 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
2723fvmpt2 6964 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ 𝑋 ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
2814, 26, 27syl2anc 585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
2928an32s 651 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ 𝐼) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
3029mpteq2dva 5210 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
31 simpr 486 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
32 ptcnp.4 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐼 ∈ 𝑉)
3332adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐼 ∈ 𝑉)
3433mptexd 7179 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
35 eqid 2737 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
3635fvmpt2 6964 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝑋 ∧ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
3731, 34, 36syl2anc 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
3830, 37eqtr4d 2780 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
3938ralrimiva 3144 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
4039adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
41 nfcv 2908 . . . . . . . . . . . . . 14 β„²π‘₯𝐼
42 nffvmpt1 6858 . . . . . . . . . . . . . 14 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)
4341, 42nfmpt 5217 . . . . . . . . . . . . 13 β„²π‘₯(π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·))
44 nffvmpt1 6858 . . . . . . . . . . . . 13 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
4543, 44nfeq 2921 . . . . . . . . . . . 12 β„²π‘₯(π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
46 fveq2 6847 . . . . . . . . . . . . . 14 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·))
4746mpteq2dv 5212 . . . . . . . . . . . . 13 (π‘₯ = 𝐷 β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)))
48 fveq2 6847 . . . . . . . . . . . . 13 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·))
4947, 48eqeq12d 2753 . . . . . . . . . . . 12 (π‘₯ = 𝐷 β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ↔ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)))
5045, 49rspc 3572 . . . . . . . . . . 11 (𝐷 ∈ 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)))
5113, 40, 50sylc 65 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·))
52 ptcnplem.6 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
5351, 52eqeltrd 2838 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
5432adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ 𝐼 ∈ 𝑉)
55 mptelixpg 8880 . . . . . . . . . 10 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)))
5654, 55syl 17 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)))
5753, 56mpbid 231 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜))
5857r19.21bi 3237 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜))
59 cnpimaex 22623 . . . . . . 7 (((π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·) ∧ (πΊβ€˜π‘˜) ∈ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
6010, 11, 58, 59syl3anc 1372 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
618, 60sylan2 594 . . . . 5 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
6261ex 414 . . . 4 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ (𝐼 ∩ π‘Š) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜))))
637, 62ralrimi 3243 . . 3 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
64 eleq2 2827 . . . . 5 (𝑒 = (π‘“β€˜π‘˜) β†’ (𝐷 ∈ 𝑒 ↔ 𝐷 ∈ (π‘“β€˜π‘˜)))
65 imaeq2 6014 . . . . . 6 (𝑒 = (π‘“β€˜π‘˜) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) = ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)))
6665sseq1d 3980 . . . . 5 (𝑒 = (π‘“β€˜π‘˜) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))
6764, 66anbi12d 632 . . . 4 (𝑒 = (π‘“β€˜π‘˜) β†’ ((𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)) ↔ (𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
6867ac6sfi 9238 . . 3 (((𝐼 ∩ π‘Š) ∈ Fin ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜))) β†’ βˆƒπ‘“(𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
694, 63, 68syl2anc 585 . 2 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘“(𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
7015ad2antrr 725 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
71 toponuni 22279 . . . . . 6 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
7270, 71syl 17 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑋 = βˆͺ 𝐽)
7372ineq1d 4176 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) = (βˆͺ 𝐽 ∩ ∩ ran 𝑓))
74 topontop 22278 . . . . . . 7 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
7515, 74syl 17 . . . . . 6 (πœ‘ β†’ 𝐽 ∈ Top)
7675ad2antrr 725 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐽 ∈ Top)
77 frn 6680 . . . . . 6 (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 β†’ ran 𝑓 βŠ† 𝐽)
7877ad2antrl 727 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ ran 𝑓 βŠ† 𝐽)
794adantr 482 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
80 ffn 6673 . . . . . . . 8 (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
8180ad2antrl 727 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
82 dffn4 6767 . . . . . . 7 (𝑓 Fn (𝐼 ∩ π‘Š) ↔ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓)
8381, 82sylib 217 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓)
84 fofi 9289 . . . . . 6 (((𝐼 ∩ π‘Š) ∈ Fin ∧ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
8579, 83, 84syl2anc 585 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ ran 𝑓 ∈ Fin)
86 eqid 2737 . . . . . 6 βˆͺ 𝐽 = βˆͺ 𝐽
8786rintopn 22274 . . . . 5 ((𝐽 ∈ Top ∧ ran 𝑓 βŠ† 𝐽 ∧ ran 𝑓 ∈ Fin) β†’ (βˆͺ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
8876, 78, 85, 87syl3anc 1372 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (βˆͺ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
8973, 88eqeltrd 2838 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽)
9012ad2antrr 725 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐷 ∈ 𝑋)
91 simpl 484 . . . . . . 7 ((𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ 𝐷 ∈ (π‘“β€˜π‘˜))
9291ralimi 3087 . . . . . 6 (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜))
9392ad2antll 728 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜))
94 eleq2 2827 . . . . . . 7 (𝑧 = (π‘“β€˜π‘˜) β†’ (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (π‘“β€˜π‘˜)))
9594ralrn 7043 . . . . . 6 (𝑓 Fn (𝐼 ∩ π‘Š) β†’ (βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜)))
9681, 95syl 17 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜)))
9793, 96mpbird 257 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧)
98 elrint 4957 . . . 4 (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ↔ (𝐷 ∈ 𝑋 ∧ βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧))
9990, 97, 98sylanbrc 584 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓))
100 nfv 1918 . . . . . . . . . 10 β„²π‘˜ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽
1017, 100nfan 1903 . . . . . . . . 9 β„²π‘˜((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽)
102 funmpt 6544 . . . . . . . . . . . . 13 Fun (π‘₯ ∈ 𝑋 ↦ 𝐴)
103 simp-4l 782 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ πœ‘)
104103, 15syl 17 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
105 simpllr 775 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽)
106 simplr 768 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ π‘˜ ∈ (𝐼 ∩ π‘Š))
107105, 106ffvelcdmd 7041 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) ∈ 𝐽)
108 toponss 22292 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘“β€˜π‘˜) ∈ 𝐽) β†’ (π‘“β€˜π‘˜) βŠ† 𝑋)
109104, 107, 108syl2anc 585 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) βŠ† 𝑋)
110106elin1d 4163 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ π‘˜ ∈ 𝐼)
111103, 110, 25syl2anc 585 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
112 dmmptg 6199 . . . . . . . . . . . . . . 15 (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐴) = 𝑋)
113111, 112syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐴) = 𝑋)
114109, 113sseqtrrd 3990 . . . . . . . . . . . . 13 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐴))
115 funimass4 6912 . . . . . . . . . . . . 13 ((Fun (π‘₯ ∈ 𝑋 ↦ 𝐴) ∧ (π‘“β€˜π‘˜) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐴)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)))
116102, 114, 115sylancr 588 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)))
117 nffvmpt1 6858 . . . . . . . . . . . . . 14 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘)
118117nfel1 2924 . . . . . . . . . . . . 13 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)
119 nfv 1918 . . . . . . . . . . . . 13 Ⅎ𝑑((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)
120 fveq2 6847 . . . . . . . . . . . . . 14 (𝑑 = π‘₯ β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯))
121120eleq1d 2823 . . . . . . . . . . . . 13 (𝑑 = π‘₯ β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
122118, 119, 121cbvralw 3292 . . . . . . . . . . . 12 (βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜))
123116, 122bitrdi 287 . . . . . . . . . . 11 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
124 inss1 4193 . . . . . . . . . . . . 13 (𝑋 ∩ ∩ ran 𝑓) βŠ† 𝑋
125 ssralv 4015 . . . . . . . . . . . . 13 ((𝑋 ∩ ∩ ran 𝑓) βŠ† 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
126124, 111, 125mpsyl 68 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
127 inss2 4194 . . . . . . . . . . . . . 14 (𝑋 ∩ ∩ ran 𝑓) βŠ† ∩ ran 𝑓
128105, 80syl 17 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
129 fnfvelrn 7036 . . . . . . . . . . . . . . . 16 ((𝑓 Fn (𝐼 ∩ π‘Š) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) β†’ (π‘“β€˜π‘˜) ∈ ran 𝑓)
130128, 106, 129syl2anc 585 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) ∈ ran 𝑓)
131 intss1 4929 . . . . . . . . . . . . . . 15 ((π‘“β€˜π‘˜) ∈ ran 𝑓 β†’ ∩ ran 𝑓 βŠ† (π‘“β€˜π‘˜))
132130, 131syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ ∩ ran 𝑓 βŠ† (π‘“β€˜π‘˜))
133127, 132sstrid 3960 . . . . . . . . . . . . 13 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (𝑋 ∩ ∩ ran 𝑓) βŠ† (π‘“β€˜π‘˜))
134 ssralv 4015 . . . . . . . . . . . . 13 ((𝑋 ∩ ∩ ran 𝑓) βŠ† (π‘“β€˜π‘˜) β†’ (βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
135133, 134syl 17 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
136 r19.26 3115 . . . . . . . . . . . . 13 (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) ↔ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
137 elinel1 4160 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) β†’ π‘₯ ∈ 𝑋)
138137, 27sylan 581 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
139138eleq1d 2823 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) ↔ 𝐴 ∈ (πΊβ€˜π‘˜)))
140139biimpd 228 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ 𝐴 ∈ (πΊβ€˜π‘˜)))
141140expimpd 455 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) β†’ ((𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) β†’ 𝐴 ∈ (πΊβ€˜π‘˜)))
142141ralimia 3084 . . . . . . . . . . . . 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 3246 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) β†’ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
148147impr 456 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
149 simpl 484 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ πœ‘)
150 eldifi 4091 . . . . . . . . . . . 12 (π‘˜ ∈ (𝐼 βˆ– π‘Š) β†’ π‘˜ ∈ 𝐼)
151137, 26sylan2 594 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
152151ralrimiva 3144 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
153149, 150, 152syl2an 597 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
154 ptcnplem.5 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ (πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
155 eleq2 2827 . . . . . . . . . . . . 13 ((πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜) β†’ (𝐴 ∈ (πΊβ€˜π‘˜) ↔ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
156155ralbidv 3175 . . . . . . . . . . . 12 ((πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜) β†’ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
157154, 156syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
158153, 157mpbird 257 . . . . . . . . . 10 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
159158ex 414 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ (𝐼 βˆ– π‘Š) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
1607, 159ralrimi 3243 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
161160adantr 482 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
162 inundif 4443 . . . . . . . . 9 ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š)) = 𝐼
163162raleqi 3314 . . . . . . . 8 (βˆ€π‘˜ ∈ ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š))βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
164 ralunb 4156 . . . . . . . 8 (βˆ€π‘˜ ∈ ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š))βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ∧ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
165163, 164bitr3i 277 . . . . . . 7 (βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ∧ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
166148, 161, 165sylanbrc 584 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
167 ralcom 3275 . . . . . 6 (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
168166, 167sylibr 233 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜))
16932ad2antrr 725 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐼 ∈ 𝑉)
170 nffvmpt1 6858 . . . . . . . . 9 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘)
171170nfel1 2924 . . . . . . . 8 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)
172 nfv 1918 . . . . . . . 8 Ⅎ𝑑((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)
173 fveq2 6847 . . . . . . . . 9 (𝑑 = π‘₯ β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
174173eleq1d 2823 . . . . . . . 8 (𝑑 = π‘₯ β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
175171, 172, 174cbvralw 3292 . . . . . . 7 (βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
176 mptexg 7176 . . . . . . . . . . 11 (𝐼 ∈ 𝑉 β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
177137, 176, 36syl2anr 598 . . . . . . . . . 10 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
178177eleq1d 2823 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
179 mptelixpg 8880 . . . . . . . . . 10 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
180179adantr 482 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
181178, 180bitrd 279 . . . . . . . 8 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
182181ralbidva 3173 . . . . . . 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 6544 . . . . 5 Fun (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
18732mptexd 7179 . . . . . . . . 9 (πœ‘ β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
188187ralrimivw 3148 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
189188ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
190 dmmptg 6199 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V β†’ dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = 𝑋)
191189, 190syl 17 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = 𝑋)
192124, 191sseqtrrid 4002 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) βŠ† dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)))
193 funimass4 6912 . . . . 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 2827 . . . . 5 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓)))
197 imaeq2 6014 . . . . . 6 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)))
198197sseq1d 3980 . . . . 5 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
199196, 198anbi12d 632 . . . 4 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)) ↔ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))))
200199rspcev 3584 . . 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 3065  βˆƒwrex 3074  Vcvv 3448   βˆ– cdif 3912   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆͺ cuni 4870  βˆ© cint 4912   ↦ cmpt 5193  dom cdm 5638  ran crn 5639   β€œ cima 5641  Fun wfun 6495   Fn wfn 6496  βŸΆwf 6497  β€“ontoβ†’wfo 6499  β€˜cfv 6501  (class class class)co 7362  Xcixp 8842  Fincfn 8890  βˆtcpt 17327  Topctop 22258  TopOnctopon 22275   CnP ccnp 22592
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-1o 8417  df-er 8655  df-map 8774  df-ixp 8843  df-en 8891  df-dom 8892  df-fin 8894  df-top 22259  df-topon 22276  df-cnp 22595
This theorem is referenced by:  ptcnp  22989
  Copyright terms: Public domain W3C validator