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

Theorem ptcnplem 23345
Description: Lemma for ptcnp 23346. (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 4228 . . . 4 (𝐼 ∩ π‘Š) βŠ† π‘Š
3 ssfi 9175 . . . 4 ((π‘Š ∈ Fin ∧ (𝐼 ∩ π‘Š) βŠ† π‘Š) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
41, 2, 3sylancl 584 . . 3 ((πœ‘ ∧ πœ“) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
5 nfv 1915 . . . . 5 β„²π‘˜πœ‘
6 ptcnplem.1 . . . . 5 β„²π‘˜πœ“
75, 6nfan 1900 . . . 4 β„²π‘˜(πœ‘ ∧ πœ“)
8 elinel1 4194 . . . . . 6 (π‘˜ ∈ (𝐼 ∩ π‘Š) β†’ π‘˜ ∈ 𝐼)
9 ptcnp.7 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·))
109adantlr 711 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·))
11 ptcnplem.3 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ (πΊβ€˜π‘˜) ∈ (πΉβ€˜π‘˜))
12 ptcnp.6 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐷 ∈ 𝑋)
1312adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ 𝐷 ∈ 𝑋)
14 simpr 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
15 ptcnp.3 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
1615adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
17 ptcnp.5 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝐹:𝐼⟢Top)
1817ffvelcdmda 7085 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ Top)
19 toptopon2 22640 . . . . . . . . . . . . . . . . . . . . 21 ((πΉβ€˜π‘˜) ∈ Top ↔ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
2018, 19sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
21 cnpf2 22974 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
2216, 20, 9, 21syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
23 eqid 2730 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ 𝑋 ↦ 𝐴) = (π‘₯ ∈ 𝑋 ↦ 𝐴)
2423fmpt 7110 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ↔ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
2522, 24sylibr 233 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
2625r19.21bi 3246 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
2723fvmpt2 7008 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ 𝑋 ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
2814, 26, 27syl2anc 582 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
2928an32s 648 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ 𝐼) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
3029mpteq2dva 5247 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
31 simpr 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ π‘₯ ∈ 𝑋)
32 ptcnp.4 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐼 ∈ 𝑉)
3332adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐼 ∈ 𝑉)
3433mptexd 7227 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
35 eqid 2730 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
3635fvmpt2 7008 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝑋 ∧ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
3731, 34, 36syl2anc 582 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
3830, 37eqtr4d 2773 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
3938ralrimiva 3144 . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
4039adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
41 nfcv 2901 . . . . . . . . . . . . . 14 β„²π‘₯𝐼
42 nffvmpt1 6901 . . . . . . . . . . . . . 14 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)
4341, 42nfmpt 5254 . . . . . . . . . . . . 13 β„²π‘₯(π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·))
44 nffvmpt1 6901 . . . . . . . . . . . . 13 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
4543, 44nfeq 2914 . . . . . . . . . . . 12 β„²π‘₯(π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
46 fveq2 6890 . . . . . . . . . . . . . 14 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·))
4746mpteq2dv 5249 . . . . . . . . . . . . 13 (π‘₯ = 𝐷 β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)))
48 fveq2 6890 . . . . . . . . . . . . 13 (π‘₯ = 𝐷 β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·))
4947, 48eqeq12d 2746 . . . . . . . . . . . 12 (π‘₯ = 𝐷 β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ↔ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)))
5045, 49rspc 3599 . . . . . . . . . . 11 (𝐷 ∈ 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)))
5113, 40, 50sylc 65 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·))
52 ptcnplem.6 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
5351, 52eqeltrd 2831 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
5432adantr 479 . . . . . . . . . 10 ((πœ‘ ∧ πœ“) β†’ 𝐼 ∈ 𝑉)
55 mptelixpg 8931 . . . . . . . . . 10 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)))
5654, 55syl 17 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ ((π‘˜ ∈ 𝐼 ↦ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·)) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)))
5753, 56mpbid 231 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ 𝐼 ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜))
5857r19.21bi 3246 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜))
59 cnpimaex 22980 . . . . . . 7 (((π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·) ∧ (πΊβ€˜π‘˜) ∈ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π·) ∈ (πΊβ€˜π‘˜)) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
6010, 11, 58, 59syl3anc 1369 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ 𝐼) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
618, 60sylan2 591 . . . . 5 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
6261ex 411 . . . 4 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ (𝐼 ∩ π‘Š) β†’ βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜))))
637, 62ralrimi 3252 . . 3 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)))
64 eleq2 2820 . . . . 5 (𝑒 = (π‘“β€˜π‘˜) β†’ (𝐷 ∈ 𝑒 ↔ 𝐷 ∈ (π‘“β€˜π‘˜)))
65 imaeq2 6054 . . . . . 6 (𝑒 = (π‘“β€˜π‘˜) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) = ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)))
6665sseq1d 4012 . . . . 5 (𝑒 = (π‘“β€˜π‘˜) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))
6764, 66anbi12d 629 . . . 4 (𝑒 = (π‘“β€˜π‘˜) β†’ ((𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜)) ↔ (𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
6867ac6sfi 9289 . . 3 (((𝐼 ∩ π‘Š) ∈ Fin ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆƒπ‘’ ∈ 𝐽 (𝐷 ∈ 𝑒 ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ 𝑒) βŠ† (πΊβ€˜π‘˜))) β†’ βˆƒπ‘“(𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
694, 63, 68syl2anc 582 . 2 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘“(𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜))))
7015ad2antrr 722 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
71 toponuni 22636 . . . . . 6 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
7270, 71syl 17 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑋 = βˆͺ 𝐽)
7372ineq1d 4210 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) = (βˆͺ 𝐽 ∩ ∩ ran 𝑓))
74 topontop 22635 . . . . . . 7 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
7515, 74syl 17 . . . . . 6 (πœ‘ β†’ 𝐽 ∈ Top)
7675ad2antrr 722 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐽 ∈ Top)
77 frn 6723 . . . . . 6 (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 β†’ ran 𝑓 βŠ† 𝐽)
7877ad2antrl 724 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ ran 𝑓 βŠ† 𝐽)
794adantr 479 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝐼 ∩ π‘Š) ∈ Fin)
80 ffn 6716 . . . . . . . 8 (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
8180ad2antrl 724 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
82 dffn4 6810 . . . . . . 7 (𝑓 Fn (𝐼 ∩ π‘Š) ↔ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓)
8381, 82sylib 217 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓)
84 fofi 9340 . . . . . 6 (((𝐼 ∩ π‘Š) ∈ Fin ∧ 𝑓:(𝐼 ∩ π‘Š)–ontoβ†’ran 𝑓) β†’ ran 𝑓 ∈ Fin)
8579, 83, 84syl2anc 582 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ ran 𝑓 ∈ Fin)
86 eqid 2730 . . . . . 6 βˆͺ 𝐽 = βˆͺ 𝐽
8786rintopn 22631 . . . . 5 ((𝐽 ∈ Top ∧ ran 𝑓 βŠ† 𝐽 ∧ ran 𝑓 ∈ Fin) β†’ (βˆͺ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
8876, 78, 85, 87syl3anc 1369 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (βˆͺ 𝐽 ∩ ∩ ran 𝑓) ∈ 𝐽)
8973, 88eqeltrd 2831 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽)
9012ad2antrr 722 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐷 ∈ 𝑋)
91 simpl 481 . . . . . . 7 ((𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ 𝐷 ∈ (π‘“β€˜π‘˜))
9291ralimi 3081 . . . . . 6 (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜))
9392ad2antll 725 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜))
94 eleq2 2820 . . . . . . 7 (𝑧 = (π‘“β€˜π‘˜) β†’ (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (π‘“β€˜π‘˜)))
9594ralrn 7088 . . . . . 6 (𝑓 Fn (𝐼 ∩ π‘Š) β†’ (βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜)))
9681, 95syl 17 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧 ↔ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)𝐷 ∈ (π‘“β€˜π‘˜)))
9793, 96mpbird 256 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧)
98 elrint 4994 . . . 4 (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ↔ (𝐷 ∈ 𝑋 ∧ βˆ€π‘§ ∈ ran 𝑓 𝐷 ∈ 𝑧))
9990, 97, 98sylanbrc 581 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓))
100 nfv 1915 . . . . . . . . . 10 β„²π‘˜ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽
1017, 100nfan 1900 . . . . . . . . 9 β„²π‘˜((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽)
102 funmpt 6585 . . . . . . . . . . . . 13 Fun (π‘₯ ∈ 𝑋 ↦ 𝐴)
103 simp-4l 779 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ πœ‘)
104103, 15syl 17 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
105 simpllr 772 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽)
106 simplr 765 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ π‘˜ ∈ (𝐼 ∩ π‘Š))
107105, 106ffvelcdmd 7086 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) ∈ 𝐽)
108 toponss 22649 . . . . . . . . . . . . . . 15 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘“β€˜π‘˜) ∈ 𝐽) β†’ (π‘“β€˜π‘˜) βŠ† 𝑋)
109104, 107, 108syl2anc 582 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) βŠ† 𝑋)
110106elin1d 4197 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ π‘˜ ∈ 𝐼)
111103, 110, 25syl2anc 582 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
112 dmmptg 6240 . . . . . . . . . . . . . . 15 (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐴) = 𝑋)
113111, 112syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ dom (π‘₯ ∈ 𝑋 ↦ 𝐴) = 𝑋)
114109, 113sseqtrrd 4022 . . . . . . . . . . . . 13 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐴))
115 funimass4 6955 . . . . . . . . . . . . 13 ((Fun (π‘₯ ∈ 𝑋 ↦ 𝐴) ∧ (π‘“β€˜π‘˜) βŠ† dom (π‘₯ ∈ 𝑋 ↦ 𝐴)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)))
116102, 114, 115sylancr 585 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)))
117 nffvmpt1 6901 . . . . . . . . . . . . . 14 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘)
118117nfel1 2917 . . . . . . . . . . . . 13 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜)
119 nfv 1915 . . . . . . . . . . . . 13 Ⅎ𝑑((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)
120 fveq2 6890 . . . . . . . . . . . . . 14 (𝑑 = π‘₯ β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) = ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯))
121120eleq1d 2816 . . . . . . . . . . . . 13 (𝑑 = π‘₯ β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
122118, 119, 121cbvralw 3301 . . . . . . . . . . . 12 (βˆ€π‘‘ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘‘) ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜))
123116, 122bitrdi 286 . . . . . . . . . . 11 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
124 inss1 4227 . . . . . . . . . . . . 13 (𝑋 ∩ ∩ ran 𝑓) βŠ† 𝑋
125 ssralv 4049 . . . . . . . . . . . . 13 ((𝑋 ∩ ∩ ran 𝑓) βŠ† 𝑋 β†’ (βˆ€π‘₯ ∈ 𝑋 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
126124, 111, 125mpsyl 68 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
127 inss2 4228 . . . . . . . . . . . . . 14 (𝑋 ∩ ∩ ran 𝑓) βŠ† ∩ ran 𝑓
128105, 80syl 17 . . . . . . . . . . . . . . . 16 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ 𝑓 Fn (𝐼 ∩ π‘Š))
129 fnfvelrn 7081 . . . . . . . . . . . . . . . 16 ((𝑓 Fn (𝐼 ∩ π‘Š) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) β†’ (π‘“β€˜π‘˜) ∈ ran 𝑓)
130128, 106, 129syl2anc 582 . . . . . . . . . . . . . . 15 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (π‘“β€˜π‘˜) ∈ ran 𝑓)
131 intss1 4966 . . . . . . . . . . . . . . 15 ((π‘“β€˜π‘˜) ∈ ran 𝑓 β†’ ∩ ran 𝑓 βŠ† (π‘“β€˜π‘˜))
132130, 131syl 17 . . . . . . . . . . . . . 14 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ ∩ ran 𝑓 βŠ† (π‘“β€˜π‘˜))
133127, 132sstrid 3992 . . . . . . . . . . . . 13 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (𝑋 ∩ ∩ ran 𝑓) βŠ† (π‘“β€˜π‘˜))
134 ssralv 4049 . . . . . . . . . . . . 13 ((𝑋 ∩ ∩ ran 𝑓) βŠ† (π‘“β€˜π‘˜) β†’ (βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
135133, 134syl 17 . . . . . . . . . . . 12 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
136 r19.26 3109 . . . . . . . . . . . . 13 (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) ↔ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)))
137 elinel1 4194 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) β†’ π‘₯ ∈ 𝑋)
138137, 27sylan 578 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) = 𝐴)
139138eleq1d 2816 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) ↔ 𝐴 ∈ (πΊβ€˜π‘˜)))
140139biimpd 228 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ 𝐴 ∈ (πΊβ€˜π‘˜)))
141140expimpd 452 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓) β†’ ((𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) β†’ 𝐴 ∈ (πΊβ€˜π‘˜)))
142141ralimia 3078 . . . . . . . . . . . . 13 (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)(𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
143136, 142sylbir 234 . . . . . . . . . . . 12 ((βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜) ∧ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
144126, 135, 143syl6an 680 . . . . . . . . . . 11 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (βˆ€π‘₯ ∈ (π‘“β€˜π‘˜)((π‘₯ ∈ 𝑋 ↦ 𝐴)β€˜π‘₯) ∈ (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
145123, 144sylbid 239 . . . . . . . . . 10 (((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) ∧ 𝐷 ∈ (π‘“β€˜π‘˜)) β†’ (((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
146145expimpd 452 . . . . . . . . 9 ((((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) ∧ π‘˜ ∈ (𝐼 ∩ π‘Š)) β†’ ((𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
147101, 146ralimdaa 3255 . . . . . . . 8 (((πœ‘ ∧ πœ“) ∧ 𝑓:(𝐼 ∩ π‘Š)⟢𝐽) β†’ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
148147impr 453 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
149 simpl 481 . . . . . . . . . . . 12 ((πœ‘ ∧ πœ“) β†’ πœ‘)
150 eldifi 4125 . . . . . . . . . . . 12 (π‘˜ ∈ (𝐼 βˆ– π‘Š) β†’ π‘˜ ∈ 𝐼)
151137, 26sylan2 591 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
152151ralrimiva 3144 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
153149, 150, 152syl2an 594 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
154 ptcnplem.5 . . . . . . . . . . . 12 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ (πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
155 eleq2 2820 . . . . . . . . . . . . 13 ((πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜) β†’ (𝐴 ∈ (πΊβ€˜π‘˜) ↔ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
156155ralbidv 3175 . . . . . . . . . . . 12 ((πΊβ€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜) β†’ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
157154, 156syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
158153, 157mpbird 256 . . . . . . . . . 10 (((πœ‘ ∧ πœ“) ∧ π‘˜ ∈ (𝐼 βˆ– π‘Š)) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
159158ex 411 . . . . . . . . 9 ((πœ‘ ∧ πœ“) β†’ (π‘˜ ∈ (𝐼 βˆ– π‘Š) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
1607, 159ralrimi 3252 . . . . . . . 8 ((πœ‘ ∧ πœ“) β†’ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
161160adantr 479 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
162 inundif 4477 . . . . . . . . 9 ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š)) = 𝐼
163162raleqi 3321 . . . . . . . 8 (βˆ€π‘˜ ∈ ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š))βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
164 ralunb 4190 . . . . . . . 8 (βˆ€π‘˜ ∈ ((𝐼 ∩ π‘Š) βˆͺ (𝐼 βˆ– π‘Š))βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ∧ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
165163, 164bitr3i 276 . . . . . . 7 (βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ↔ (βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜) ∧ βˆ€π‘˜ ∈ (𝐼 βˆ– π‘Š)βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜)))
166148, 161, 165sylanbrc 581 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
167 ralcom 3284 . . . . . 6 (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)𝐴 ∈ (πΊβ€˜π‘˜))
168166, 167sylibr 233 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜))
16932ad2antrr 722 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ 𝐼 ∈ 𝑉)
170 nffvmpt1 6901 . . . . . . . . 9 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘)
171170nfel1 2917 . . . . . . . 8 β„²π‘₯((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)
172 nfv 1915 . . . . . . . 8 Ⅎ𝑑((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)
173 fveq2 6890 . . . . . . . . 9 (𝑑 = π‘₯ β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯))
174173eleq1d 2816 . . . . . . . 8 (𝑑 = π‘₯ β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
175171, 172, 174cbvralw 3301 . . . . . . 7 (βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
176 mptexg 7224 . . . . . . . . . . 11 (𝐼 ∈ 𝑉 β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
177137, 176, 36syl2anr 595 . . . . . . . . . 10 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) = (π‘˜ ∈ 𝐼 ↦ 𝐴))
178177eleq1d 2816 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
179 mptelixpg 8931 . . . . . . . . . 10 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
180179adantr 479 . . . . . . . . 9 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
181178, 180bitrd 278 . . . . . . . 8 ((𝐼 ∈ 𝑉 ∧ π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
182181ralbidva 3173 . . . . . . 7 (𝐼 ∈ 𝑉 β†’ (βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘₯) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
183175, 182bitrid 282 . . . . . 6 (𝐼 ∈ 𝑉 β†’ (βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
184169, 183syl 17 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘₯ ∈ (𝑋 ∩ ∩ ran 𝑓)βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ (πΊβ€˜π‘˜)))
185168, 184mpbird 256 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
186 funmpt 6585 . . . . 5 Fun (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
18732mptexd 7227 . . . . . . . . 9 (πœ‘ β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
188187ralrimivw 3148 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
189188ad2antrr 722 . . . . . . 7 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V)
190 dmmptg 6240 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑋 (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ V β†’ dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = 𝑋)
191189, 190syl 17 . . . . . 6 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) = 𝑋)
192124, 191sseqtrrid 4034 . . . . 5 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (𝑋 ∩ ∩ ran 𝑓) βŠ† dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)))
193 funimass4 6955 . . . . 5 ((Fun (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) ∧ (𝑋 ∩ ∩ ran 𝑓) βŠ† dom (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
194186, 192, 193sylancr 585 . . . 4 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ βˆ€π‘‘ ∈ (𝑋 ∩ ∩ ran 𝑓)((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π‘‘) ∈ Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
195185, 194mpbird 256 . . 3 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))
196 eleq2 2820 . . . . 5 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ (𝐷 ∈ 𝑧 ↔ 𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓)))
197 imaeq2 6054 . . . . . 6 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) = ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)))
198197sseq1d 4012 . . . . 5 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜) ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
199196, 198anbi12d 629 . . . 4 (𝑧 = (𝑋 ∩ ∩ ran 𝑓) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)) ↔ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))))
200199rspcev 3611 . . 3 (((𝑋 ∩ ∩ ran 𝑓) ∈ 𝐽 ∧ (𝐷 ∈ (𝑋 ∩ ∩ ran 𝑓) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ (𝑋 ∩ ∩ ran 𝑓)) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
20189, 99, 195, 200syl12anc 833 . 2 (((πœ‘ ∧ πœ“) ∧ (𝑓:(𝐼 ∩ π‘Š)⟢𝐽 ∧ βˆ€π‘˜ ∈ (𝐼 ∩ π‘Š)(𝐷 ∈ (π‘“β€˜π‘˜) ∧ ((π‘₯ ∈ 𝑋 ↦ 𝐴) β€œ (π‘“β€˜π‘˜)) βŠ† (πΊβ€˜π‘˜)))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
20269, 201exlimddv 1936 1 ((πœ‘ ∧ πœ“) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (πΊβ€˜π‘˜)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539  βˆƒwex 1779  β„²wnf 1783   ∈ wcel 2104  βˆ€wral 3059  βˆƒwrex 3068  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆͺ cuni 4907  βˆ© cint 4949   ↦ cmpt 5230  dom cdm 5675  ran crn 5676   β€œ cima 5678  Fun wfun 6536   Fn wfn 6537  βŸΆwf 6538  β€“ontoβ†’wfo 6540  β€˜cfv 6542  (class class class)co 7411  Xcixp 8893  Fincfn 8941  βˆtcpt 17388  Topctop 22615  TopOnctopon 22632   CnP ccnp 22949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-fin 8945  df-top 22616  df-topon 22633  df-cnp 22952
This theorem is referenced by:  ptcnp  23346
  Copyright terms: Public domain W3C validator