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

Theorem ptpjpre1 22107
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 6663 . . . . . . . 8 (𝑘 = 𝐼 → (𝑤𝑘) = (𝑤𝐼))
2 fveq2 6663 . . . . . . . . 9 (𝑘 = 𝐼 → (𝐹𝑘) = (𝐹𝐼))
32unieqd 4840 . . . . . . . 8 (𝑘 = 𝐼 (𝐹𝑘) = (𝐹𝐼))
41, 3eleq12d 2904 . . . . . . 7 (𝑘 = 𝐼 → ((𝑤𝑘) ∈ (𝐹𝑘) ↔ (𝑤𝐼) ∈ (𝐹𝐼)))
5 vex 3495 . . . . . . . . . . 11 𝑤 ∈ V
65elixp 8456 . . . . . . . . . 10 (𝑤X𝑘𝐴 (𝐹𝑘) ↔ (𝑤 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑤𝑘) ∈ (𝐹𝑘)))
76simprbi 497 . . . . . . . . 9 (𝑤X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑤𝑘) ∈ (𝐹𝑘))
8 ptpjpre1.1 . . . . . . . . 9 𝑋 = X𝑘𝐴 (𝐹𝑘)
97, 8eleq2s 2928 . . . . . . . 8 (𝑤𝑋 → ∀𝑘𝐴 (𝑤𝑘) ∈ (𝐹𝑘))
109adantl 482 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ 𝑤𝑋) → ∀𝑘𝐴 (𝑤𝑘) ∈ (𝐹𝑘))
11 simplrl 773 . . . . . . 7 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ 𝑤𝑋) → 𝐼𝐴)
124, 10, 11rspcdva 3622 . . . . . 6 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ 𝑤𝑋) → (𝑤𝐼) ∈ (𝐹𝐼))
1312fmpttd 6871 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑤𝑋 ↦ (𝑤𝐼)):𝑋 (𝐹𝐼))
14 ffn 6507 . . . . 5 ((𝑤𝑋 ↦ (𝑤𝐼)):𝑋 (𝐹𝐼) → (𝑤𝑋 ↦ (𝑤𝐼)) Fn 𝑋)
15 elpreima 6820 . . . . 5 ((𝑤𝑋 ↦ (𝑤𝐼)) Fn 𝑋 → (𝑧 ∈ ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) ↔ (𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈)))
1613, 14, 153syl 18 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑧 ∈ ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) ↔ (𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈)))
17 fveq1 6662 . . . . . . . . 9 (𝑤 = 𝑧 → (𝑤𝐼) = (𝑧𝐼))
18 eqid 2818 . . . . . . . . 9 (𝑤𝑋 ↦ (𝑤𝐼)) = (𝑤𝑋 ↦ (𝑤𝐼))
19 fvex 6676 . . . . . . . . 9 (𝑧𝐼) ∈ V
2017, 18, 19fvmpt 6761 . . . . . . . 8 (𝑧𝑋 → ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) = (𝑧𝐼))
2120eleq1d 2894 . . . . . . 7 (𝑧𝑋 → (((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈 ↔ (𝑧𝐼) ∈ 𝑈))
2221pm5.32i 575 . . . . . 6 ((𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈) ↔ (𝑧𝑋 ∧ (𝑧𝐼) ∈ 𝑈))
238eleq2i 2901 . . . . . . . . 9 (𝑧𝑋𝑧X𝑘𝐴 (𝐹𝑘))
24 vex 3495 . . . . . . . . . 10 𝑧 ∈ V
2524elixp 8456 . . . . . . . . 9 (𝑧X𝑘𝐴 (𝐹𝑘) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)))
2623, 25bitri 276 . . . . . . . 8 (𝑧𝑋 ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)))
2726anbi1i 623 . . . . . . 7 ((𝑧𝑋 ∧ (𝑧𝐼) ∈ 𝑈) ↔ ((𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)) ∧ (𝑧𝐼) ∈ 𝑈))
28 anass 469 . . . . . . 7 (((𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)) ∧ (𝑧𝐼) ∈ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)))
2927, 28bitri 276 . . . . . 6 ((𝑧𝑋 ∧ (𝑧𝐼) ∈ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)))
3022, 29bitri 276 . . . . 5 ((𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)))
31 simprl 767 . . . . . . . . . . . . 13 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (𝑧𝐼) ∈ 𝑈)
32 fveq2 6663 . . . . . . . . . . . . . 14 (𝑘 = 𝐼 → (𝑧𝑘) = (𝑧𝐼))
33 iftrue 4469 . . . . . . . . . . . . . 14 (𝑘 = 𝐼 → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) = 𝑈)
3432, 33eleq12d 2904 . . . . . . . . . . . . 13 (𝑘 = 𝐼 → ((𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ↔ (𝑧𝐼) ∈ 𝑈))
3531, 34syl5ibrcom 248 . . . . . . . . . . . 12 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (𝑘 = 𝐼 → (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
36 simprr 769 . . . . . . . . . . . . 13 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (𝑧𝑘) ∈ (𝐹𝑘))
37 iffalse 4472 . . . . . . . . . . . . . 14 𝑘 = 𝐼 → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) = (𝐹𝑘))
3837eleq2d 2895 . . . . . . . . . . . . 13 𝑘 = 𝐼 → ((𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ↔ (𝑧𝑘) ∈ (𝐹𝑘)))
3936, 38syl5ibrcom 248 . . . . . . . . . . . 12 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (¬ 𝑘 = 𝐼 → (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
4035, 39pm2.61d 180 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ ((𝑧𝐼) ∈ 𝑈 ∧ (𝑧𝑘) ∈ (𝐹𝑘))) → (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))
4140expr 457 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ (𝑧𝐼) ∈ 𝑈) → ((𝑧𝑘) ∈ (𝐹𝑘) → (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
4241ralimdv 3175 . . . . . . . . 9 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) ∧ (𝑧𝐼) ∈ 𝑈) → (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) → ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
4342expimpd 454 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (((𝑧𝐼) ∈ 𝑈 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)) → ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
4443ancomsd 466 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈) → ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
45 elssuni 4859 . . . . . . . . . . . . 13 (𝑈 ∈ (𝐹𝐼) → 𝑈 (𝐹𝐼))
4645ad2antll 725 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → 𝑈 (𝐹𝐼))
4733, 3sseq12d 3997 . . . . . . . . . . . 12 (𝑘 = 𝐼 → (if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ⊆ (𝐹𝑘) ↔ 𝑈 (𝐹𝐼)))
4846, 47syl5ibrcom 248 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑘 = 𝐼 → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ⊆ (𝐹𝑘)))
49 ssid 3986 . . . . . . . . . . . 12 (𝐹𝑘) ⊆ (𝐹𝑘)
5037, 49eqsstrdi 4018 . . . . . . . . . . 11 𝑘 = 𝐼 → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ⊆ (𝐹𝑘))
5148, 50pm2.61d1 181 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ⊆ (𝐹𝑘))
5251sseld 3963 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → (𝑧𝑘) ∈ (𝐹𝑘)))
5352ralimdv 3175 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → ∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘)))
5434rspcv 3615 . . . . . . . . 9 (𝐼𝐴 → (∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → (𝑧𝐼) ∈ 𝑈))
5554ad2antrl 724 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → (𝑧𝐼) ∈ 𝑈))
5653, 55jcad 513 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) → (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)))
5744, 56impbid 213 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈) ↔ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
5857anbi2d 628 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑧 Fn 𝐴 ∧ (∀𝑘𝐴 (𝑧𝑘) ∈ (𝐹𝑘) ∧ (𝑧𝐼) ∈ 𝑈)) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))))
5930, 58syl5bb 284 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑧𝑋 ∧ ((𝑤𝑋 ↦ (𝑤𝐼))‘𝑧) ∈ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))))
6016, 59bitrd 280 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑧 ∈ ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))))
6124elixp 8456 . . 3 (𝑧X𝑘𝐴 if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑧𝑘) ∈ if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
6260, 61syl6bbr 290 . 2 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → (𝑧 ∈ ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) ↔ 𝑧X𝑘𝐴 if(𝑘 = 𝐼, 𝑈, (𝐹𝑘))))
6362eqrdv 2816 1 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝐼𝐴𝑈 ∈ (𝐹𝐼))) → ((𝑤𝑋 ↦ (𝑤𝐼)) “ 𝑈) = X𝑘𝐴 if(𝑘 = 𝐼, 𝑈, (𝐹𝑘)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wral 3135  wss 3933  ifcif 4463   cuni 4830  cmpt 5137  ccnv 5547  cima 5551   Fn wfn 6343  wf 6344  cfv 6348  Xcixp 8449  Topctop 21429
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ixp 8450
This theorem is referenced by:  ptpjpre2  22116  ptbasfi  22117
  Copyright terms: Public domain W3C validator