Metamath Proof Explorer


Theorem upixp

Description: Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses upixp.1 X=bACb
upixp.2 P=wAxXxw
Assertion upixp ARBSaAFa:BCa∃!hh:BXaAFa=Pah

Proof

Step Hyp Ref Expression
1 upixp.1 X=bACb
2 upixp.2 P=wAxXxw
3 mptexg BSuBsAFsuV
4 3 3ad2ant2 ARBSaAFa:BCauBsAFsuV
5 ffvelrn Fa:BCauBFauCa
6 5 expcom uBFa:BCaFauCa
7 6 ralimdv uBaAFa:BCaaAFauCa
8 7 impcom aAFa:BCauBaAFauCa
9 8 3ad2antl3 ARBSaAFa:BCauBaAFauCa
10 fveq2 a=sFa=Fs
11 10 fveq1d a=sFau=Fsu
12 fveq2 a=sCa=Cs
13 11 12 eleq12d a=sFauCaFsuCs
14 13 cbvralvw aAFauCasAFsuCs
15 9 14 sylib ARBSaAFa:BCauBsAFsuCs
16 simpl1 ARBSaAFa:BCauBAR
17 mptelixpg ARsAFsusACssAFsuCs
18 16 17 syl ARBSaAFa:BCauBsAFsusACssAFsuCs
19 15 18 mpbird ARBSaAFa:BCauBsAFsusACs
20 fveq2 b=sCb=Cs
21 20 cbvixpv bACb=sACs
22 1 21 eqtri X=sACs
23 19 22 eleqtrrdi ARBSaAFa:BCauBsAFsuX
24 23 fmpttd ARBSaAFa:BCauBsAFsu:BX
25 nfv aAR
26 nfv aBS
27 nfra1 aaAFa:BCa
28 25 26 27 nf3an aARBSaAFa:BCa
29 fveq2 s=aFs=Fa
30 29 fveq1d s=aFsu=Fau
31 eqid sAFsu=sAFsu
32 fvex FsuV
33 30 31 32 fvmpt3i aAsAFsua=Fau
34 33 adantl ARBSaAFa:BCaaAsAFsua=Fau
35 34 mpteq2dv ARBSaAFa:BCaaAuBsAFsua=uBFau
36 23 adantlr ARBSaAFa:BCaaAuBsAFsuX
37 eqidd ARBSaAFa:BCaaAuBsAFsu=uBsAFsu
38 fveq2 w=axw=xa
39 38 mpteq2dv w=axXxw=xXxa
40 fvex CbV
41 40 rgenw bACbV
42 ixpexg bACbVbACbV
43 41 42 ax-mp bACbV
44 1 43 eqeltri XV
45 44 mptex xXxwV
46 39 2 45 fvmpt3i aAPa=xXxa
47 46 adantl ARBSaAFa:BCaaAPa=xXxa
48 fveq1 x=sAFsuxa=sAFsua
49 36 37 47 48 fmptco ARBSaAFa:BCaaAPauBsAFsu=uBsAFsua
50 rsp aAFa:BCaaAFa:BCa
51 50 3ad2ant3 ARBSaAFa:BCaaAFa:BCa
52 51 imp ARBSaAFa:BCaaAFa:BCa
53 52 feqmptd ARBSaAFa:BCaaAFa=uBFau
54 35 49 53 3eqtr4rd ARBSaAFa:BCaaAFa=PauBsAFsu
55 54 ex ARBSaAFa:BCaaAFa=PauBsAFsu
56 28 55 ralrimi ARBSaAFa:BCaaAFa=PauBsAFsu
57 simprl ARBSaAFa:BCah:BXaAFa=Pahh:BX
58 57 feqmptd ARBSaAFa:BCah:BXaAFa=Pahh=uBhu
59 simplrr ARBSaAFa:BCah:BXaAFa=PahuBaAFa=Pah
60 fveq2 a=sPa=Ps
61 60 coeq1d a=sPah=Psh
62 10 61 eqeq12d a=sFa=PahFs=Psh
63 62 rspccva aAFa=PahsAFs=Psh
64 59 63 sylan ARBSaAFa:BCah:BXaAFa=PahuBsAFs=Psh
65 64 fveq1d ARBSaAFa:BCah:BXaAFa=PahuBsAFsu=Pshu
66 fvco3 h:BXuBPshu=Pshu
67 57 66 sylan ARBSaAFa:BCah:BXaAFa=PahuBPshu=Pshu
68 67 adantr ARBSaAFa:BCah:BXaAFa=PahuBsAPshu=Pshu
69 fveq2 w=sxw=xs
70 69 mpteq2dv w=sxXxw=xXxs
71 70 2 45 fvmpt3i sAPs=xXxs
72 71 adantl ARBSaAFa:BCah:BXaAFa=PahuBsAPs=xXxs
73 72 fveq1d ARBSaAFa:BCah:BXaAFa=PahuBsAPshu=xXxshu
74 ffvelrn h:BXuBhuX
75 57 74 sylan ARBSaAFa:BCah:BXaAFa=PahuBhuX
76 fveq1 x=huxs=hus
77 eqid xXxs=xXxs
78 fvex xsV
79 76 77 78 fvmpt3i huXxXxshu=hus
80 75 79 syl ARBSaAFa:BCah:BXaAFa=PahuBxXxshu=hus
81 80 adantr ARBSaAFa:BCah:BXaAFa=PahuBsAxXxshu=hus
82 73 81 eqtrd ARBSaAFa:BCah:BXaAFa=PahuBsAPshu=hus
83 65 68 82 3eqtrd ARBSaAFa:BCah:BXaAFa=PahuBsAFsu=hus
84 83 mpteq2dva ARBSaAFa:BCah:BXaAFa=PahuBsAFsu=sAhus
85 75 1 eleqtrdi ARBSaAFa:BCah:BXaAFa=PahuBhubACb
86 ixpfn hubACbhuFnA
87 85 86 syl ARBSaAFa:BCah:BXaAFa=PahuBhuFnA
88 dffn5 huFnAhu=sAhus
89 87 88 sylib ARBSaAFa:BCah:BXaAFa=PahuBhu=sAhus
90 84 89 eqtr4d ARBSaAFa:BCah:BXaAFa=PahuBsAFsu=hu
91 90 mpteq2dva ARBSaAFa:BCah:BXaAFa=PahuBsAFsu=uBhu
92 58 91 eqtr4d ARBSaAFa:BCah:BXaAFa=Pahh=uBsAFsu
93 92 ex ARBSaAFa:BCah:BXaAFa=Pahh=uBsAFsu
94 93 alrimiv ARBSaAFa:BCahh:BXaAFa=Pahh=uBsAFsu
95 feq1 h=uBsAFsuh:BXuBsAFsu:BX
96 coeq2 h=uBsAFsuPah=PauBsAFsu
97 96 eqeq2d h=uBsAFsuFa=PahFa=PauBsAFsu
98 97 ralbidv h=uBsAFsuaAFa=PahaAFa=PauBsAFsu
99 95 98 anbi12d h=uBsAFsuh:BXaAFa=PahuBsAFsu:BXaAFa=PauBsAFsu
100 99 eqeu uBsAFsuVuBsAFsu:BXaAFa=PauBsAFsuhh:BXaAFa=Pahh=uBsAFsu∃!hh:BXaAFa=Pah
101 4 24 56 94 100 syl121anc ARBSaAFa:BCa∃!hh:BXaAFa=Pah