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

Theorem ptpjpre1 21582
Description: The preimage of a projection function can be expressed as an indexed cartesian product. (Contributed by Mario Carneiro, 6-Feb-2015.)
Hypothesis
Ref Expression
ptpjpre1.1 𝑋 = X𝑘𝐴 (𝐹𝑘)
Assertion
Ref Expression
ptpjpre1 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) = X𝑘𝐴 if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))
Distinct variable groups:   𝑤,𝑘,𝐴   𝑘,𝐹,𝑤   𝑘,𝐼,𝑤   𝑈,𝑘,𝑤   𝑘,𝑉,𝑤   𝑤,𝑋
Allowed substitution hint:   𝑋(𝑘)

Proof of Theorem ptpjpre1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6402 . . . . . . . 8 (𝑘 = 𝐼 → (𝑤𝑘) = (𝑤𝐼))
2 fveq2 6402 . . . . . . . . 9 (𝑘 = 𝐼 → (𝐹𝑘) = (𝐹𝐼))
32unieqd 4633 . . . . . . . 8 (𝑘 = 𝐼 (𝐹𝑘) = (𝐹𝐼))
41, 3eleq12d 2875 . . . . . . 7 (𝑘 = 𝐼 → ((𝑤𝑘) ∈ (𝐹𝑘) ↔ (𝑤𝐼) ∈ (𝐹𝐼)))
5 vex 3390 . . . . . . . . . . 11 𝑤 ∈ V
65elixp 8146 . . . . . . . . . 10 (𝑤X𝑘𝐴 (𝐹𝑘) ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑤𝑘) ∈ (𝐹𝑘)))
76simprbi 486 . . . . . . . . 9 (𝑤X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑤𝑘) ∈ (𝐹𝑘))
8 ptpjpre1.1 . . . . . . . . 9 𝑋 = X𝑘𝐴 (𝐹𝑘)
97, 8eleq2s 2899 . . . . . . . 8 (𝑤𝑋 → ∀𝑘𝐴 (𝑤𝑘) ∈ (𝐹𝑘))
109adantl 469 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ 𝑤𝑋) → ∀𝑘𝐴 (𝑤𝑘) ∈ (𝐹𝑘))
11 simplrl 786 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ 𝑤𝑋) → 𝐼𝐴)
124, 10, 11rspcdva 3504 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ 𝑤𝑋) → (𝑤𝐼) ∈ (𝐹𝐼))
1312fmpttd 6601 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑤𝑋 ↦ (𝑤𝐼)):𝑋 (𝐹𝐼))
14 ffn 6250 . . . . 5 ((𝑤𝑋 ↦ (𝑤𝐼)):𝑋 (𝐹𝐼) → (𝑤𝑋 ↦ (𝑤𝐼)) Fn 𝑋)
15 elpreima 6553 . . . . 5 ((𝑤𝑋 ↦ (𝑤𝐼)) Fn 𝑋 → (𝑧 ∈ ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) ↔ (𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈)))
1613, 14, 153syl 18 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑧 ∈ ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) ↔ (𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈)))
17 fveq1 6401 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤𝐼) = (𝑧𝐼))
18 eqid 2802 . . . . . . . . 9 (𝑤𝑋 ↦ (𝑤𝐼)) = (𝑤𝑋 ↦ (𝑤𝐼))
19 fvex 6415 . . . . . . . . 9 (𝑧𝐼) ∈ V
2017, 18, 19fvmpt 6497 . . . . . . . 8 (𝑧𝑋 → ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) = (𝑧𝐼))
2120eleq1d 2866 . . . . . . 7 (𝑧𝑋 → (((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈 ↔ (𝑧𝐼) ∈ 𝑈))
2221pm5.32i 566 . . . . . 6 ((𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈) ↔ (𝑧𝑋 ∧ (𝑧𝐼) ∈ 𝑈))
238eleq2i 2873 . . . . . . . . 9 (𝑧𝑋𝑧X𝑘𝐴 (𝐹𝑘))
24 vex 3390 . . . . . . . . . 10 𝑧 ∈ V
2524elixp 8146 . . . . . . . . 9 (𝑧X𝑘𝐴 (𝐹𝑘) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)))
2623, 25bitri 266 . . . . . . . 8 (𝑧𝑋 ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)))
2726anbi1i 612 . . . . . . 7 ((𝑧𝑋 ∧ (𝑧𝐼) ∈ 𝑈) ↔ ((𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)) ∧ (𝑧𝐼) ∈ 𝑈))
28 anass 456 . . . . . . 7 (((𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)) ∧ (𝑧𝐼) ∈ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)))
2927, 28bitri 266 . . . . . 6 ((𝑧𝑋 ∧ (𝑧𝐼) ∈ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)))
3022, 29bitri 266 . . . . 5 ((𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)))
31 simprl 778 . . . . . . . . . . . . 13 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (𝑧𝐼) ∈ 𝑈)
32 fveq2 6402 . . . . . . . . . . . . . 14 (𝑘 = 𝐼 → (𝑧𝑘) = (𝑧𝐼))
33 iftrue 4279 . . . . . . . . . . . . . 14 (𝑘 = 𝐼 → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) = 𝑈)
3432, 33eleq12d 2875 . . . . . . . . . . . . 13 (𝑘 = 𝐼 → ((𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ↔ (𝑧𝐼) ∈ 𝑈))
3531, 34syl5ibrcom 238 . . . . . . . . . . . 12 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (𝑘 = 𝐼 → (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
36 simprr 780 . . . . . . . . . . . . 13 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (𝑧𝑘) ∈ (𝐹𝑘))
37 iffalse 4282 . . . . . . . . . . . . . 14 𝑘 = 𝐼 → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) = (𝐹𝑘))
3837eleq2d 2867 . . . . . . . . . . . . 13 𝑘 = 𝐼 → ((𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ↔ (𝑧𝑘) ∈ (𝐹𝑘)))
3936, 38syl5ibrcom 238 . . . . . . . . . . . 12 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (¬ 𝑘 = 𝐼 → (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
4035, 39pm2.61d 171 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))
4140expr 446 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ (𝑧𝐼) ∈ 𝑈) → ((𝑧𝑘) ∈ (𝐹𝑘) → (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
4241ralimdv 3147 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ (𝑧𝐼) ∈ 𝑈) → (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) → ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
4342expimpd 443 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (((𝑧𝐼) ∈ 𝑈 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)) → ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
4443ancomsd 453 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈) → ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
45 elssuni 4654 . . . . . . . . . . . . 13 (𝑈 ∈ (𝐹𝐼) → 𝑈 (𝐹𝐼))
4645ad2antll 711 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → 𝑈 (𝐹𝐼))
4733, 3sseq12d 3825 . . . . . . . . . . . 12 (𝑘 = 𝐼 → (if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ⊆ (𝐹𝑘) ↔ 𝑈 (𝐹𝐼)))
4846, 47syl5ibrcom 238 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑘 = 𝐼 → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ⊆ (𝐹𝑘)))
49 ssid 3814 . . . . . . . . . . . 12 (𝐹𝑘) ⊆ (𝐹𝑘)
5037, 49syl6eqss 3846 . . . . . . . . . . 11 𝑘 = 𝐼 → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ⊆ (𝐹𝑘))
5148, 50pm2.61d1 172 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ⊆ (𝐹𝑘))
5251sseld 3791 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → (𝑧𝑘) ∈ (𝐹𝑘)))
5352ralimdv 3147 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)))
5434rspcv 3494 . . . . . . . . 9 (𝐼𝐴 → (∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → (𝑧𝐼) ∈ 𝑈))
5554ad2antrl 710 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → (𝑧𝐼) ∈ 𝑈))
5653, 55jcad 504 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)))
5744, 56impbid 203 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈) ↔ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
5857anbi2d 616 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑧 Fn 𝐴 ∧ (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))))
5930, 58syl5bb 274 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))))
6016, 59bitrd 270 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑧 ∈ ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))))
6124elixp 8146 . . 3 (𝑧X𝑘𝐴 if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
6260, 61syl6bbr 280 . 2 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑧 ∈ ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) ↔ 𝑧X𝑘𝐴 if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
6362eqrdv 2800 1 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) = X𝑘𝐴 if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2155  wral 3092  wss 3763  ifcif 4273   cuni 4623  cmpt 4916  ccnv 5304  cima 5308   Fn wfn 6090  wf 6091  cfv 6095  Xcixp 8139  Topctop 20905
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pr 5090
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-ral 3097  df-rex 3098  df-rab 3101  df-v 3389  df-sbc 3628  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-uni 4624  df-br 4838  df-opab 4900  df-mpt 4917  df-id 5213  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-fv 6103  df-ixp 8140
This theorem is referenced by:  ptpjpre2  21591  ptbasfi  21592
  Copyright terms: Public domain W3C validator